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
1 MPII - Max-Planck-Institut für Informatik
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.
keyword : calcul de superposition superposition calculus superposition simplification
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

istex

Identifiers

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

95

 

Contact                    Legal Notice                    Personal Data