Research Group Formal Methods and Deduction Prof. Dr. J. Avenhaus

 Automated Theorem Proving

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.