Term schemata are iterated terms with exponents, e.g.
fn(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(succ2n(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
to download DEI. A short system description is also
DEI is freely distributed. It is available under the