Research Group Logo CS Dept.
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.

Follow the links to
Impressum RG Formal Methods and Deduction Department of Informatics Technical University of Kaiserslautern Valid HTML 4.01!

Last Update: Wednesday, 26-Oct-05 08:59:21 GMT