Digital Repository

An Interactive Theorem Prover for First-Order Dynamic Logic

DSpace/Manakin Repository

Show simple item record Das, Tuhin Kanti 2012-10-11T17:03:53Z 2012-10-11T17:03:53Z 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. en_US
dc.language.iso eng en_US
dc.publisher Brock University en_US
dc.subject Dynamic Logic en_US
dc.subject Hoare logic en_US
dc.subject Program verification en_US
dc.title An Interactive Theorem Prover for First-Order Dynamic Logic en_US
dc.type Electronic Thesis or Dissertation en_US M.Sc. Computer Science en_US Masters en_US
dc.contributor.department Department of Computer Science en_US Faculty of Mathematics and Science en_US
dc.embargo.terms None en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search The Repository


My Account


About the Digital Repository