Re: Toward a common syntax for writing proofs

David Musser (musser@cs.rpi.edu)
Mon, 18 Mar 96 10:43:25 EST

> Another related problem is an explication of the notion "proof".
> The usual definition of proof as " a finite sequence of one or more
> formulas each of which either is an axiom or is immediatedly inferred
> from preceding formulas in the sequence by means of one of the rules
> of inference" is unsatisfactory for our goals because:
>
> 1) This definition is good for "bottom-up" proofs, but real proofs may
> be "top-down", that is, a formula in a top-down proof may be inferred
> using also some succeding formulas;
>
> 2) A real proof may contain not only formulas but also some definitions;

You might find the following paper useful in this regard:

D. Kapur, D. Musser, and X. Nie, ``An Overview of the Tecton Proof
System,'' Theoretical Computer Science, Vol. 133, pp. 307-339,
October 24, 1994.

This paper includes a definition of proofs as forests of trees that
have additional links between subtrees (corresponding to the use of
one goal as a lemma in the proof of another) making them DAG-like.
This proof representation allows for different levels of detail in a
proof, since a node may represent not only an axiom or inference rule
but also the use of an inference mechanism that produces a proof tree.
It also can represent multiple proof attempts of the same goal.

-- 
David R. Musser
 Rensselaer Polytechnic Institute	518 276-8660
 Computer Science Department		FAX: 518 276-4033
 Troy, NY 12180				musser@cs.rpi.edu
             http://www.cs.rpi.edu/~musser