Technische Universität München, Fakultät für Informatik
Lehrstuhl Informatik IV, Research Group Automated Reasoning

E Example Specifications

Here are three simple examples of E input files. The distribution has a large number of additional examples. Note that all lines starting with # are comments. For more examples, you can browse the TPTP problem library (note that E can now directly parse classic TPTP format as well as TPTP-3 format).

Rewriting: Equational Specification of a Group

This is the classic example for completion as given by Knuth and Bendix in their famous paper Simple Word Problems in Universal Algebras from 1970. E 0.9 can complete this specification using about 1/30th of a second of cputime on an Apple TiBook 1GHZ (but note that time resolution is getting critical for such simple examples), including the overhead for parsing, I/O, and generation of a suitable term ordering. This is pretty good even for a normal state-of-the-art (i.e. not Waldmeister, which is far beyond the state of the art ;-) prover for pure unit equality problems.

#--------------------------------------------------------------------
# Equational specification of a group. This specification does have
# models, i.e. it cannot be refuted (and the prover will note this). 
#
# It uses only unit clauses in infix-equational notation.
#

# There exists a right-neutral element 0.
f(X,0)=X.

# For each X, there is a right inverse element i(X).
f(X,i(X))=0.

# f is associative.
f(f(X,Y),Z)=f(X,f(Y,Z)).

You can add hypothesises to this example to make it into a proof problem. As goal clauses are negated in refutational theorem proving, all-quantified variables are turned into skolem constants:

# Hypothesis: Right inverse is also left inverse

<- f(i(a),a) = 0.

For some people it might be more intuitive to represent the goal as an explicitly negated atom:

# A nother possible hypothesis: Multiplication with inverse element is
# commutative.

~f(a,i(a)) = f(i(a),a).

Both ways to state the theorem are possible in the LOP-dialect that is used by E, as would be the use of != in the atom. In strict LOP, only the prefix equal() predicate is supported, as shown in the next example.

Group Theory: Properties of Finite Groups

This example is taken from the TPTP problem library. It has been automatically translated using the tptp2x utility and shows how the prefix-notation for equations is used. The goal is represented by an all-negative clause. This problem can be solved by E's default strategy in about 1/10 of a second on my powerbook.

#--------------------------------------------------------------------------
# File     : GRP121-1 : TPTP v2.1.0. Released v1.2.0.
# Domain   : Group Theory
# Problem  : Derive right identity from a single axiom for groups order 4
# Version  : [Wos96] (equality) axioms.
# English  : 

# Refs     : [Wos96] Wos (1996), The Automation of Reasoning: An Experiment 
# Source   : [OTTER]
# Names    : groups.exp4.in part 3 [OTTER]

# Status   : unsatisfiable
# Rating   : 0.60 v2.1.0, 0.43 v2.0.0
# Syntax   : Number of clauses    :    3 (   0 non-Horn;   3 unit;   2 RR)
#            Number of literals   :    3 (   3 equality)
#            Maximal clause size  :    1 (   1 average)
#            Number of predicates :    1 (   0 propositional; 2-2 arity)
#            Number of functors   :    3 (   2 constant; 0-2 arity)
#            Number of variables  :    3 (   0 singleton)
#            Maximal term depth   :    6 (   2 average)

# Comments : 
#          : tptp2X -f setheo:sign -t rm_equality:rstfp GRP121-1.p 
#--------------------------------------------------------------------------
# single_axiom, axiom.
equal(multiply(Y, multiply(multiply(Y, multiply(multiply(Y, Y), multiply(X, Z)))
, multiply(Z, multiply(Z, Z)))), X) <- .

# single_axiom2, axiom.
equal(multiply(identity, identity), identity) <- .

# prove_order3, conjecture.
 <- equal(multiply(a, identity), a).

#--------------------------------------------------------------------------

Classical Puzzles: The Steamroller

This is a standard problem using no equality at all. E 0.9 proves the problem in about 1/5th of a second with its default strategy.

Note that the literals in the clauses are non-equational. E automatically translates them to equational literals internally, i.e.the axiom

animal(X) <- wolf(X).

is internally represented as

equal(animal(X), $true) <- equal(wolf(X), $true).

for the special constant symbol $true.

#--------------------------------------------------------------------------
# File     : PUZ031-1 : TPTP v2.0.0. Released v1.0.0.
# Domain   : Puzzles
# Problem  : Schubert's Steamroller
# Version  : Special.
# English  : Wolves, foxes, birds, caterpillars, and snails are animals, 
#            and there are some of each of them. Also there are some 
#            grains, and grains are plants. Every animal either likes 
#            to eat all plants or all animals much smaller than itself 
#            that like to eat some plants.
#            Caterpillars and snails are much smaller than birds, which 
#            are much smaller than foxes, which in turn are much smaller 
#            than wolves. Wolves do not like to eat foxes or grains, while 
#            birds like to eat caterpillars but not snails. Caterpillars 
#            and snails like to eat some plants. Therefore there 
#            is an animal that likes to eat a grain eating animal.

# Refs     : Stickel M. (1986), Schubert's Steamroller Problem: 
#            Formulations and Solution, Journal of Automated Reasoning 
#            2(2), 89-104.
#          : Pelletier F.J. (1986), Seventy-Five Problems for Testing 
#            Automatic Theorem Provers, Journal of Automated Reasoning 
#            2(2), 191-216.
#          : Wang T-C., Bledsoe W.W. (1987), Hierarchical Deduction,
#            Journal of Automated Deduction 3(1), 35-77.
#          : Manthey R., Bry F. (1988), SATCHMO: a theorem prover 
#            implemented in Prolog, In Lusk E., Overbeek R. (Eds), 
#            Proceedings of the 9th International Conference on Automated 
#            Deduction (Argonne, IL, 1988), (Lecture Notes in Computer 
#            Science 310), Springer-Verlag, New York, NY, 415-434.
# Source   : [Pelletier, 1986]
# Names    : Pelletier 47 [Pelletier, 1986]
#          : steamroller.ver1.in [ANL]
#          : steam.in [OTTER]
#          : SST [Wang & Bledsoe, 1987]

# Status   : unsatisfiable
# Rating   : 0.00 v2.0.0
# Syntax   : Number of clauses    :   26 (   1 non-Horn;   6 unit;  26 RR)
#            Number of literals   :   63 (   0 equality)
#            Maximal clause size  :    8 (   2 average)
#            Number of predicates :   10 (   0 propositional; 1-2 arity)
#            Number of functors   :    8 (   6 constant; 0-1 arity)
#            Number of variables  :   33 (   0 singleton)
#            Maximal term depth   :    2 (   1 average)

# Comments : This problem is named after Len Schubert.
#          : tptp2X: -fsetheo:sign PUZ031-1.p 
#--------------------------------------------------------------------------
#clausename wolf_is_an_animal
animal(X) <- 
    wolf(X).

#clausename fox_is_an_animal
animal(X) <- 
    fox(X).

#clausename bird_is_an_animal
animal(X) <- 
    bird(X).

#clausename caterpillar_is_an_animal
animal(X) <- 
    caterpillar(X).

#clausename snail_is_an_animal
animal(X) <- 
    snail(X).

#clausename there_is_a_wolf
wolf(a_wolf) <- .

#clausename there_is_a_fox
fox(a_fox) <- .

#clausename there_is_a_bird
bird(a_bird) <- .

#clausename there_is_a_caterpillar
caterpillar(a_caterpillar) <- .

#clausename there_is_a_snail
snail(a_snail) <- .

#clausename there_is_a_grain
grain(a_grain) <- .

#clausename grain_is_a_plant
plant(X) <- 
    grain(X).

#clausename eating_habits
eats(Animal, Plant);
eats(Animal, Small_animal) <- 
    animal(Animal),
    plant(Plant),
    animal(Small_animal),
    plant(Other_plant),
    much_smaller(Small_animal, Animal),
    eats(Small_animal, Other_plant).

#clausename caterpillar_smaller_than_bird
much_smaller(Catapillar, Bird) <- 
    caterpillar(Catapillar),
    bird(Bird).

#clausename snail_smaller_than_bird
much_smaller(Snail, Bird) <- 
    snail(Snail),
    bird(Bird).

#clausename bird_smaller_than_fox
much_smaller(Bird, Fox) <- 
    bird(Bird),
    fox(Fox).

#clausename fox_smaller_than_wolf
much_smaller(Fox, Wolf) <- 
    fox(Fox),
    wolf(Wolf).

#clausename wolfs_dont_eat_foxes
 <- wolf(Wolf),
    fox(Fox),
    eats(Wolf, Fox).

#clausename wolfs_dont_eat_grain
 <- wolf(Wolf),
    grain(Grain),
    eats(Wolf, Grain).

#clausename bird_eats_caterpillar
eats(Bird, Catapillar) <- 
    bird(Bird),
    caterpillar(Catapillar).

#clausename bird_dont_eat_snail
 <- bird(Bird),
    snail(Snail),
    eats(Bird, Snail).

#clausename caterpillar_food_is_a_plant
plant(caterpillar_food_of(Catapillar)) <- 
    caterpillar(Catapillar).

#clausename caterpillar_eats_caterpillar_food
eats(Catapillar, caterpillar_food_of(Catapillar)) <- 
    caterpillar(Catapillar).

#clausename snail_food_is_a_plant
plant(snail_food_of(Snail)) <- 
    snail(Snail).

#clausename snail_eats_snail_food
eats(Snail, snail_food_of(Snail)) <- 
    snail(Snail).

#clausename conjecture
 <- animal(Animal),
    animal(Grain_eater),
    grain(Grain),
    eats(Animal, Grain_eater),
    eats(Grain_eater, Grain).

Stephan Schulz,schulz@informatik.tu-muenchen.de, 7.12.1998