Name
Title | ||
|---|---|---|
Superposition with equivalence reasoning and delayed clause normal form transformation |
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.ic.2004.10.010 | Information & Computation |
Keywords | DocType | Volume |
practical experience,normal form transformation,equivalence reasoning,superposition calculus,02.10.ab,automated theorem proving,set theory,smaller side,deduction,68t15,paramodulation,03b35,clause-normal-form transformation,logical equivalence,first-order logic,simplification inference,completeness proof,delayed clause,saturate system,arbitrary formula,superposition,rewriting,normal form | Journal | 199 |
Issue | ISSN | Citations |
1-2 | Information and Computation | 12 |
PageRank | References | Authors |
0.92 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Harald Ganzinger | 1 | 1513 | 155.21 |
| Jürgen Stuber | 2 | 84 | 7.16 |
| franz baader | 3 | 34 | 2.97 |