swMATH ID: 7192
Software Authors: Stojanović, Sana; Pavlović, Vesna; Janičić, Predrag
Description: 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.
Homepage: http://rd.springer.com/chapter/10.1007/978-3-642-25070-5_12
Keywords: geometric theorem proving; coherent logic
Related Software: Coq; GCLC; TPTP; GEX; GeoGebra; Isar; GATP; JGEX; TGTP; OpenGeoProver; GeoThms; GCLCprover; GeoProof; Cinderella; gcl; E Theorem Prover; VAMPIRE; Sledgehammer; HOL Light; WGL
Cited in: 12 Publications

Citations by Year