Analysis and Representation of Equational Proofs
Generated by a Distributed Completion Based Proof System

Joerg Denzinger, Stephan Schulz
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, GERMANY
E-mail: denzinge@informatik.uni-kl.de,
        schulz@informatik.tu-muenchen.de (updated)

Abstract

Automatic proof systems are becoming more and more powerful.
However, the proofs generated by these systems are not met with
wide acceptance, because they are presented in a way
inappropriate for human understanding.

In this paper we pursue two different, but related, aims. First
we describe methods to structure and transform equational proofs
in a way that they conform to human reading conventions. We
develop algorithms to impose a hierarchical structure on proof
protocols from completion based proof systems and to generate
equational chains from them.

Our second aim is to demonstrate the difficulties of obtaining
such protocols from distributed proof systems and to present our
solution to these problems for provers using the TEAMWORK
method. We also show that proof systems using this method can
give considerable help in structuring the proof listing in a way
analogous to human behaviour.

In addition to theoretical results we also include descriptions
on algorithms, implementation notes, examples and data on a
variety of examples.

Keywords

proof presentation, distributed proofs, teamwork, proof
structuring, equational proofs

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1994/papers/
file: Denzinger.SR-94-05.ps.Z