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

Superposition with Equivalence Reasoning andDelayed Clause Normal Form Transformation

Harald Ganzinger Jürgen Stuber 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This report describes a superposition calculus where quantifiers are eliminated lazily. Superposition and simplification inferences may employ equivalences that have arbitrary formulas at their smaller side. A closely related calculus is implemented in the Saturate system and has shown useful on many examples, in particular in set theory. The report presents a completeness proof and reports on practical experience obtained with the Saturate system.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 6:40:52 PM
Last modification on : Friday, February 4, 2022 - 3:34:35 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:36:25 PM


  • HAL Id : inria-00071750, version 1



Harald Ganzinger, Jürgen Stuber. Superposition with Equivalence Reasoning andDelayed Clause Normal Form Transformation. [Research Report] RR-4835, INRIA. 2003, pp.23. ⟨inria-00071750⟩



Record views


Files downloads