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.
Cite
CITATION STYLE
Ganzinger, H., & Stuber, J. (2003). Superposition with equivalence reasoning and delayed clause normal form transformation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 335–349). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
