Show simple item record

dc.contributor.authorDas, Tuhin Kanti
dc.date.accessioned2012-10-11T17:03:53Z
dc.date.available2012-10-11T17:03:53Z
dc.date.issued2012-10-11
dc.identifier.urihttp://hdl.handle.net/10464/4116
dc.description.abstractDynamic 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.isoengen_US
dc.publisherBrock Universityen_US
dc.subjectDynamic Logicen_US
dc.subjectHoare logicen_US
dc.subjectProgram verificationen_US
dc.titleAn Interactive Theorem Prover for First-Order Dynamic Logicen_US
dc.typeElectronic Thesis or Dissertationen_US
dc.degree.nameM.Sc. Computer Scienceen_US
dc.degree.levelMastersen_US
dc.contributor.departmentDepartment of Computer Scienceen_US
dc.degree.disciplineFaculty of Mathematics and Scienceen_US
dc.embargo.termsNoneen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record