Skip to Main content Skip to Navigation
Conference papers

Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation

Harald Ganzinger 1 Jürgen Stuber 2
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper 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 paper presents a completeness proof and reports on practical experience obtained with the Saturate system.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00099710
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:40:30 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

Links full text

Identifiers

Collections

Citation

Harald Ganzinger, Jürgen Stuber. Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. 19th International Conference on Automated Deduction - CADE-19, 2003, Miami Beach, FL, United States. pp.335-349, ⟨10.1007/978-3-540-45085-6_31⟩. ⟨inria-00099710⟩

Share

Metrics

Record views

95