Sciweavers

CADE
2004
Springer
14 years 4 months ago
Modular Proof Systems for Partial Functions with Weak Equality
The paper presents a modular superposition calculus for the combination of first-order theories involving both total and partial functions. Modularity means that inferences are pu...
Harald Ganzinger, Viorica Sofronie-Stokkermans, Uw...
CSL
2007
Springer
14 years 5 months ago
Integrating Linear Arithmetic into Superposition Calculus
Abstract. We present a method of integrating linear rational arithmetic into superposition calculus for first-order logic. One of our main results is completeness of the resulting...
Konstantin Korovin, Andrei Voronkov
CADE
2009
Springer
15 years 1 days ago
Superposition and Model Evolution Combined
We present a new calculus for first-order theorem proving with equality, ME+Sup, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality)...
Peter Baumgartner, Uwe Waldmann
CADE
2009
Springer
15 years 1 days ago
Decidability Results for Saturation-Based Model Building
Abstract. Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termi...
Matthias Horbach, Christoph Weidenbach