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

The Lattice Proof

On this page you can find supplementing material to our paper: "Herbrand Sequent Extraction".

In this paper we demonstrate the usefulness of a feature of CERES, namely the extraction of Herbrand sequents, in the analysis of a simple proof about lattices. It is shown that Herbrand sequent extraction can help humans to understand computer-generated proofs, because they summarize the creative content of first-order proofs, which lies in the instantiations chosen for the quantified variables. With this information, a human can construct an informal mathematical argument that corresponds to the formal proof.

The end-sequent of the lattice proof formalizes the statement: All L1-lattices are L2-lattices.

L1-lattices are semi-lattices satisfying the additional condition that meet and join correspond to orders that are inverse to each other. L2-lattices are semi-lattices for which meet and join satisfy absorption laws.

The original lattice proof is an indirect proof composed of two subproofs concatenated by a cut-rule. The first is a proof that all L1-lattices are L3-lattices. The second is a proof that all L3-lattices are L2-lattices.

An L3-lattice is a partially ordered set satisfying two conditions that guarantee the existence of a greatest lower bound and a lowest upper bound for any two elements of the set.

CERES was used to transform this indirect proof with cuts into a direct proof, which does not use the auxiliary notion of L3-lattice, in atomic-cut-normal form (ACNF). Then a Herbrand sequent was extracted from the ACNF and used to analyze the ACNF, obtaining its corresponding informal mathematical arguments.

It turned out that the extracted Herbrand sequent still contains a redundancy information. The simplification is performed in formula (logical) level of the sequent. After the simplification the irrelevant for the validity of the seuquent formulas are marked. If all formulas of a formula occurrence are marked, then the formula occurrence is droped from the sequent.

The example starts with a formalization of the proof in the HandyLK language and compiling it with HLK to obtain an LK-proof in XML format that can be read by CERES. The output of CERES, containing the ACNF and the extracted Herbrand sequent, is also saved in XML format. The XML files lattice.xml and lattice-out.xml can be displayed with ProofTool. The simplified in term- and formula level Herbrand sequent can be viewed by ProofTool as well.

Below is the list of commands that were used to execute HLK and CERES:

$ hlk -o lattice.xml lattice.hlk p

$ hlk --ceres -o lattice-in.xml lattice.hlk p

$ touch empty.trs

$ ceres -sk -cs -ac -h -pr -rp -shs empty.trs lattice-in.xml p lattice-out.xml