A coherent logic based geometry theorem prover capable of producing formal and readable proofs A theorem prover for coherent logic, called ArgoCLP, is presented. It is applied to geometry proofs. Coherent logic is a fragment of first-order logic. The structure of the formulae is restricted to the universal quantification of an implication in which the antecedent is a conjunction of atoms and the succedent is a disjunction of existentially quantified formulae which are conjunctions of atoms.par Coherent logic offers different advantages in the context of geometric theorem proving. Firstly it is powerful enough to formulate the geometric problems, secondly it makes use of a constructive calculus, and thirdly the proofs generated can be transformed into a human readable format (much more easily than those generated by methods like Wu’s method). The calculus is made efficient by refinements such as having redundant axioms in the hierarchy of explored geometric statements and a special treatment for symmetrical predicate symbols.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Quaresma, Pedro: Towards an intelligent and dynamic geometry book (2017)
- Dyckhoff, Roy: Invited talk: coherentisation of first-order logic (2015)
- Dyckhoff, Roy; Negri, Sara: Geometrisation of first-order logic (2015)
- Marinković, Vesna; Janičić, Predrag; Schreck, Pascal: Computer theorem proving for verifiable solving of geometric construction problems (2015)
- Stojanović Đurđević, Sana; Narboux, Julien; Janičić, Predrag: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry (2015)
- Stojanović, Sana; Narboux, Julien; Bezem, Marc; Janičić, Predrag: A vernacular for coherent logic (2014)
- Stojanović, Sana; Pavlović, Vesna; Janičić, Predrag: A coherent logic based geometry theorem prover capable of producing formal and readable proofs (2011)