HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)

The Tape Proof

The end-sequent formalizes the statement: on a tape with infinitely many cells, which are all labelled by either 0 or 1, there are two cells labelled by the same number.f(n)=0 expresses that the cell with number n is labelled by 0. Indexing of cells is done by number terms defined over 0,1 and +.

The example is taken from Urban (C. Urban: Classical Logic and Computation, Ph.D. Thesis, University of Cambridge Computer Laboratory, 2000.). It is formalized in LK but we use the extensions by equality rules and definition introduction to give a simpler formalization and allow an easier analysis of the proof.

The example proof uses two lemmas:

These lemmas are eliminiated by CERES and a more direct argument is obtained in the resulting proof.

The example starts with a formalization of the proof as an HLK file. From this file a CERES input file gets generated via the HLK compiler. The XML files tape.xml and tape-out.xml can be displayed with the ProofTool.

$ hlk -o tape.xml tape.hlk the-proof

$ hlk --ceres -o tape-in.xml tape.hlk the-proof

$ ceres --cutelim -ac tape-in.xml the-proof tape-out.xml

The intermediary input and output files of the automated theorem prover Otter are: tape.in and tape.out.