{"id":{"repo_id":"brock","oai_identifier":"oai:brocku.scholaris.ca:10464/4116"},"canonical_url":"https://search.dev.ndltd.org/etd/brock/oai:brocku.scholaris.ca:10464/4116","repository":{"repo_id":"brock","name":"Brock University","base_url":"https://brocku.scholaris.ca/server/oai/request"},"display":{"title":"An Interactive Theorem Prover for First-Order Dynamic Logic","abstract":"Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.","abstract_html":"Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.","abstract_has_math":false,"creators":["Das, Tuhin Kanti"],"institution":"Brock University","degree_name":"M.Sc. Computer Science","degree_level":"Masters","degree_discipline":"Faculty of Mathematics and Science","degree_department":"Department of Computer Science","school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012-10-11","date_published":"2012-10-11","updated_at":"2026-07-24T01:23:18Z","subjects":["Dynamic Logic","Hoare logic","Program verification"],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10464/4116","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.department","label":"Department","values":["Department of Computer Science"]},{"key":"dc:creator","label":"Author","values":["Das, Tuhin Kanti"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2012-10-11T17:03:53Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2012-10-11T17:03:53Z"]},{"key":"dc:date.issued","label":"Date","values":["2012-10-11"]},{"key":"dc:type","label":"Dc Type","values":["Electronic Thesis or Dissertation"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Faculty of Mathematics and Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.Sc. Computer Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Brock University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Dynamic Logic","Hoare logic","Program verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10464/4116"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used."]},{"key":"dc:title","label":"Title","values":["An Interactive Theorem Prover for First-Order Dynamic Logic"]}]}],"canonical_facts":{"dc:contributor.department":["Department of Computer Science"],"dc:creator":["Das, Tuhin Kanti"],"dc:date.accessioned":["2012-10-11T17:03:53Z"],"dc:date.available":["2012-10-11T17:03:53Z"],"dc:date.issued":["2012-10-11"],"dc:description.abstract":["Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used."],"dc:identifier.uri":["http://hdl.handle.net/10464/4116"],"dc:language.iso":["eng"],"dc:subject":["Dynamic Logic","Hoare logic","Program verification"],"dc:title":["An Interactive Theorem Prover for First-Order Dynamic Logic"],"dc:type":["Electronic Thesis or Dissertation"],"thesis:degree_discipline":["Faculty of Mathematics and Science"],"thesis:degree_level":["Masters"],"thesis:degree_name":["M.Sc. Computer Science"],"thesis:institution_name":["Brock University"]},"updated_at":"2026-07-24T01:23:18Z"}