HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Book sections

Orderings in Automated Theorem Proving

Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper is intended to give an introduction to several techniques used in automated theorem proving, and based on the concept of ordering on terms and more generally on formulas. Different orderings and their automation are presented and several applications are considered. We show how orderings provide a way to incorporate equality decision procedures in theorem provers. We also illustrate their fundamental role to automatise proofs by induction and proofs by refutation. Finally, we explain how they allow pruning the search space of a theorem prover by defining strategies to restrict application of inference rules.
Document type :
Book sections
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Monday, September 25, 2006 - 5:01:12 PM
Last modification on : Friday, February 4, 2022 - 3:31:39 AM


  • HAL Id : inria-00098418, version 1



Hélène Kirchner. Orderings in Automated Theorem Proving. Hoffman, Frederick. Mathematical Aspects of Artificial Intelligence, American Mathematical Society, pp.55-95, 1998, Proceedings of Symposia in Applied Mathematics. ⟨inria-00098418⟩



Record views