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.