Analysis and Transformation of Equational Proofs

                  Stephan Schulz

Abstract:

Automatic proof systems have steadily gained power in the last
couple of years. However, they are barely used outside the
research environment, and the generated proofs are not generally
accepted by mathematicians

Moreover, the powerful search heuristics used in this systems
are not very well understood, and additional improvements can be
expected if the proof processes can be analyzed in detail.

This report tries to aleviate these problems for the case of a
unfailing-completion based proof system for pure equational
logic.

It first introduces the basic concepts of unfailing completion
and suggests a proof procedure for equational logic. The
language PCL (Proof Communication Language) for the exchange of
protocols of equational proof processes is defined.

Building on this description of proofs, tools for the analysis
of proofs, the introduction of lemmata and the transformation of
proofs into a calculus of equational chains are developed and
described in detail. First results are presented.

The appedices present a number of examples.