Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00071750
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:40:52 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:36:25 PM

Identifiers

  • HAL Id : inria-00071750, version 1

Collections

Citation

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

Share

Metrics

Record views

221

Files downloads

360