po2hr - Otter Proof Object to LaTeX converter

Summary

This is a Lisp module for converting the Lisp-formatted proof object outputted by the first-order-logic-based automatic theorem prover Otter into LaTeX files for producing human-readable proof documents. In Otter, output of the proof object is enabled with the set(build_proof_object). option. This module's features include:

Conversion of disjunctive normal form back into implicative form
Elimination of repetitive, unnecessary, and some obvious steps
Typesetting of unary and binary operators, with precedence levels
Reorganization of proof to improve flow and reduce average reference distance.

To use it, simply load it and invoke print-latex-proof on the proof object outputted by Otter, as shown below. You may wish to customize the operator tables or *MIN-INLINE-OTTER-STATEMENT-SIZE*, both near the beginning of the file, for your particular application.

(LOAD "po2hr.lisp")(print-latex-proof '(
(1 (input) ((not (FUNCTION v0)) (not (FUNCTION (inverse v0))) (ONEONE v0)) (1))
(2 (input) ((not (ONEONE (0)))) (2))
(3 (input) ((FUNCTION (0))) (3))
(4 (input) ((equal (inverse (0)) (0))) (4))
(5 (instantiate 1 ((v0 . (0)))) ((not (FUNCTION (0))) (not (FUNCTION (inverse (0)))) (ONEONE (0))) NIL)
(6 (paramod 4 (1 1) 5 (2 1 1)) ((not (FUNCTION (0))) (not (FUNCTION (0))) (ONEONE (0))) NIL)
(7 (propositional 6) ((not (FUNCTION (0))) (ONEONE (0))) (7))
(8 (resolve 7 (1) 3 (1)) ((ONEONE (0))) (8))
(9 (resolve 2 (1) 8 (1)) () (9))
)
)

View output of this example: (tex) (ps) (pdf)

View output of a much larger example: (tex) (ps) (pdf)

Download

Warning: po2hr does not work correctly in gcl and some other Lisps, due to lack of support for READTABLE-CASE, which is needed in order to preserve case in the Otter proof object. However, if you must use it in one of these systems, just remove the line containing READTABLE-CASE, and you will get some, albeit ugly, output.

The implementation is contained entirely within the file po2hr.lisp, and has no external dependencies. Each function and global variables is documented within:

po2hr.lisp (view html)

To-Do

In the future, I need to do some of these:

Handle statements that are so long that they don't fit on the page.
Find a way to automatically add the theorem statement.
Convert Skolem functions back into existential statements.
Automatically change trivial proof-by-contradiction of an assumption to a direct proof.
Your suggestions

Back to code

Back to main page

All text and images, but not necessarily linked material, on this page ©1998-2006 Derrick Coetzee and Moonflare and may not be reproduced or used for any purpose without prior written permission except where otherwise indicated.