The task of an automated theorem prover is to deduce from a set of facts, the
axioms, another given fact, the goal. If this is possible,
then the goal is a theorem.
There are very different ways how the term "deduce" can be defined. Among the
factors determining this definition is what you allow as facts. In our
DISCOUNT system, the facts are equations of terms
and a deduction is applying such an equation in order to "substitute equal
by equal". Since the variables in the terms of the equations (as, for example,
x,y and z) can be substituted by any term, there are many possibilities for
applying equations. So, we get hard search problems.
The picture on this page shows a proof generated by DISCOUNT. The introductions
and the partition of the proof by lemmata were solely generated by
DISCOUNT itself.
The part of the term an equation is applied to is underscored and the term
it is substituted with is in bold face. For each step, the equation applied
and the substitutions to variables are given.
Follow the links to
