General procedure used

In this document I used OTTER [1] to produce a semi-automated ultra-formal verification of a main technical lemma in Holmes [2]. To keep track of the main line of reasoning, I started all OTTER runs from a single, growing input file. This file started out with only the axioms of TRC from Holmes and grew according to the process (executed by hand) whose main loop is shown here:

  1. A new definition is introduced as a demodulator of the form newName = term where newName is a new constant (an atomic term not beginning with u, v, w, x, y, or z), and term is a term of TRC built from the constants p1, p2, abst, eq and any constants that were introduced by definitions in earlier iterations of this loop. The term term was produced from a lambda-expression using a program I wrote to implement the abstraction algorithm given in Holmes [2]. In the present document, whenever such a definition is introduced, the actual demodulator input to OTTER is listed first, then an explanation of the rationale for the definition is given. I then repeat the following sub-loop to prove various properties of term:

    1. Negate the property and add one or more clauses from the negation to the set of support, adding all other clauses from the negation to the usable list.
    2. When a refutation has been found, add the positive statement of the property to the usable list for use in all future runs.
    3. Immediately after the new usable item(s), insert a copy of OTTER's proof as well as an HTML link to the OTTER output file.


When the entire argument was complete, I added explanatory text to the input file and wrote a Java program to convert the input file into a collection of HTML files, automatically inserting links from each input clause in each proof to the place earlier in the file where the clause was first introduced, where either a proof is given or the clause is clearly identified as a definition or an axiom of TRC. This relieves human readers from part of the tedium of checking the generated proof. The end result is the present document, which is generated in both printable and web-browsable form.
up show outline