| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 9656877 | Information and Computation | 2005 | 21 Pages |
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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Harald Ganzinger, Jürgen Stuber,