Implementation of a Proof Assistant in Prolog | Andreas Hussing
| | Abstract | In an intuitionistic logic the law of excluded middle is disregarded. However it is shown that if an intuitionistic logic accepts the axioms of choice and extensionality, then the law of excluded middle can be derived in that very logic. A logic that accepts these two axioms will therefore always be classical and cannot be intuitionistic. In this thesis the intuitionistic higher order logic HOLPro is presented, and it is shown that this logic turns out classical when adding the axioms of choice and extensionality to it. It is shown by deriving the law of excluded middle and Peano arithmetic from HOLPro. The modus ponens rule is needed to use the axiom of choice to make HOLPro classical, and it is therefore derived in the logic. An implementation of the logic has been made in Prolog. The types, terms, axioms and derived rules of the logic have been implemented to show, how the deduction rules of HOLPro can be used to validate a formula from one or more other formulas, which is the purpose of a proof assistant. | | Type | Bachelor thesis [Academic thesis] | | Year | 2011 | | Publisher | Technical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk | | Address | Asmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark | | Series | IMM-B.Sc.-2011-12 | | Note | | | Electronic version(s) | [pdf] | | Publication link | http://www.imm.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|