An Interactive Theorem Prover for First-Order Dynamic Logic

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.

Name thesis:degree_name

M.Sc. Computer Science

Level thesis:degree_level

Masters

Discipline thesis:degree_discipline

Faculty of Mathematics and Science

Department dc:contributor.department

Department of Computer Science

Grantor

Brock University

Year dc:date.issued

2012

Author dc:creator

• Das, Tuhin Kanti

• Dynamic Logic
• Hoare logic
• Program verification

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/10464/4116

OAI identifier oai:identifier

oai:brocku.scholaris.ca:10464/4116