ArgoCLP 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 Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year A coherent logic based geometry theorem prover capable of producing formal and readable proofs. Zbl 1252.68264Stojanović, Sana; Pavlović, Vesna; Janičić, Predrag 2011 all top 5 Cited by 17 Authors 6 Janičić, Predrag 3 Narboux, Julien 3 Quaresma, Pedro 2 Dyckhoff, Roy 2 Marinković, Vesna 2 Stojanović Đurđević, Sana 2 Stojanović, Sana 1 Baeta, Nuno 1 Bezem, Marc 1 Fleuriot, Jacques D. 1 Graziani, Pierluigi 1 Kovács, Zoltán 1 Negri, Sara 1 Nikolić, Mladen 1 Pavlović, Vesna 1 Santos, Vanda 1 Schreck, Pascal Cited in 4 Serials 3 Annals of Mathematics and Artificial Intelligence 2 Mathematics in Computer Science 1 Journal of Symbolic Computation 1 The Bulletin of Symbolic Logic Cited in 4 Fields 10 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 4 Geometry (51-XX) 1 Mathematics education (97-XX) Citations by Year