dei

DEI (standing for Deduction with the E-prover and I-terms) is a superposition-based theorem prover for first-order logic with equality. It is the first (to the best of our knowledge) automated reasoning system able to handle term schemata. It is an extension of the E Equational Theorem Prover developed by Stephan Schulz.

Term schemata are iterated terms with exponents, e.g. fⁿ(a), where n may be a natural number, but also an arithmetic variable or even a (linear) expression.
The use of term schemata (usually possible only at the meta-level) significantly increases the expressive power of first-order logic and prevents divergence in some cases: for instance the infinite sequence even(0), even(succ(succ(0))),even(succ(succ(succ(succ(0))))),... can be denoted as a unique unit clause: even(succ²ⁿ(0)) or in DEI's syntax: even($iterm(succ(@),0)^{n+n}). n is a variable, which can denote any natural number.

DEI is developed and maintained by H. Bensaïd, from the CAPP team of the Laboratory of Informatics of Grenoble (LIG) and from the INPT of Morocco, under the supervision of R. Caferra and N. Peltier

Click here to download DEI. A short system description is also available.

DEI is freely distributed. It is available under the GNU GENERAL PUBLIC LICENSE.