Superposition with Equivalence Reasoning and Delayed Clause Normal Form 
Transformation

Ganzinger, Harald; Stuber, Jürgen; Baader, Franz

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation

MPS-Authors

/persons/resource/persons44474

Ganzinger, Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45567

Stuber, Jürgen
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44050

Baader, Franz
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Ganzinger, H., & Stuber, J. (2003). Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. In Automated Deduction, CADE-19: 19th International Conference on Automated Deduction (pp. 335-349). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2E48-F

Abstract

The 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.