Easier Typesetting of Proof Trees

A Frontend to the LaTeX Bussproofs package with accompanying VIM Plugin

Recently I wanted to typeset a quite large proof tree in LaTeX using the Bussproofs package. As usual, I didn’t do this by hand editing text files, but by using the convenient LyXproofs library for doing this in a what-you-see-is-what-you-mean manner within LyX. Still, I didn’t quite like the experience; the nice math support of LyX came at the cost of the tree no longer fitting into the window; also, I didn’t want to go the step back to plain LaTeX editing.

The solution I came up with is a new, lisp-like syntax for specifying proof trees along with a rendering engine translating trees specified in this syntax to LaTeX, either for including into existing files or for outputting a standalone file suitable for direct compilation.

Example

The following sample show a (nonsense) proof tree written in that syntax:

(macro implies 0 "\Longrightarrow")
(defop neg "\neg " 40 prefix)
(defop modality "\left[#1\right]#2" 40 param)
(defop land " \land " 30 infix)
(defop text "\textrm{#1}" 99999 param)
(defop list ", " 10 infix)
(defop lor " \lor " 20 infix)
(defop seq "\implies " 0 infix)

(proof (
    (lor "asdf" (lor "asdf" (neg "asdf")))
    (seq "" (modality "p" "\phi"))
    (neg (lor "p" "q"))
    (land (lor "p" "q") (lor "q" "p"))
    (lor (land "p" "q") (land "q" "p"))
    (lor "asdf" (lor "asdf" "asdf")) <- "That's ``a'' right label!"
    "FancySplitRule 1" -> (seq "" (list (neg "p") (neg "q") (lor "p" "q")))
    (
        "subtree1"
        "test"
        (
            "test"
            (seq (lor "p" (neg "q")) "succedent")
            (neg "p")
        )
    )
    (
        "subtree2"
        "test"
    )
    (
        (text "And a third branch!!!")
    )
))

This is rendered to the following tree:

Proof Tree

The definition of operators allows for a freely choosable degree of abstraction; in the most basic case, you only indicate the structure of the tree with parantheses and use LaTeX strings for the rest; in the extreme case, the whole tree will consist of operators in lisp notation. It’s up to you!

VIM Plugin

To make it more convenient, I’ve built a VIM plugin that helps you writing proof trees. It sets the syntax highlighting / folding to lisp and provides input for using the Tagbar plugin to obtain a nice outline. Furthermore, there is a keyboard shortcut for initiating rendering to LaTeX followed by the compilation to a PDF. Here’s a screenshot of VIM with the plugin installed:

VIM prooftree plugin

Links

Both projects are available on GitHub: