Superposition calculus
Encyclopedia
The superposition calculus is a calculus for reasoning
in equational first-order logic
. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of (unfailing) Knuth-Bendix completion
. It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full clausal logic). As most first-order calculi, superposition tries to show the unsatisfiability of a set of first-order clauses, i.e. it performs proofs by refutation. Superposition is refutation-complete — given unlimited resources and a fair derivation strategy, every unsatisfiable clause set can eventually be proved to be unsatisfiable.
As of 2007, most of the (state-of-the-art) theorem provers for first-order logic
are based on superposition (e.g. the E equational theorem prover
), although only a few implement the pure calculus.
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
in equational first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of (unfailing) Knuth-Bendix completion
Knuth-Bendix completion algorithm
The Knuth–Bendix completion algorithm is an algorithm for transforming a set of equations into a confluent term rewriting system...
. It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full clausal logic). As most first-order calculi, superposition tries to show the unsatisfiability of a set of first-order clauses, i.e. it performs proofs by refutation. Superposition is refutation-complete — given unlimited resources and a fair derivation strategy, every unsatisfiable clause set can eventually be proved to be unsatisfiable.
As of 2007, most of the (state-of-the-art) theorem provers for first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
are based on superposition (e.g. the E equational theorem prover
E equational theorem prover
E is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem...
), although only a few implement the pure calculus.
Implementations
- EE equational theorem proverE is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem...
- SPASSSPASS theorem proverSPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus....
- VampireVampire theorem proverVampire is an automatic theorem prover for first-order classical logic developed in the Computer Science Department of the University of Manchester byProf. Andrei Voronkov together with Kryštof Hoder and previously with Dr. Alexandre Riazanov...
- Waldmeister
- Ayane at Google Code