Prolog Code:

Example Queries:

What is this?

The above is basically Jens Otten’s prover from the “Build Your Own First-Order Prover” at CADE 2019 in particular lecture 2. I added a tracing parameter to it so that I can draw the sequent using MathJax. Note that my javascript is looking for a query variable called Proof in order to draw the output.

What is a Proof Anyway?

Proofs are actions or things that convince you of something.

How’s that for really nailing it down?

Some examples of stuff that might be considered “proof”:

  • A solution to a set of linear equations is proof that they can be solved.
  • A dual vector is proof of optimality of a linear program.
  • A convincing English paragraph is proof.
  • Use of a cryptographic key can prove your identity.
  • A trace of a complete search program that failed to find a solution is proof of its nonexistence.

There is a sense that for something to be a proof requires it to be relatively easy to check the proof.

A narrower view of proof is that proof is a pile of formal manipulations of syntax. One thing that you can prove is the truth of a proposition combined using logical connectives.

A sequent is a structure that represents a partial state of a proof. It contains a breakdown of formula. $ A,B,C,… \vdash D,E,F,…$. Spiritually a sequent represents the knowledge or judgement that the conjunction of the antecedents implies one of the consequents, but a sequent could be just considered pure syntax, merely a dead data structure to hold a pile of meaningless symbols.

The sequent proof viewed from the bottom up is a stepwise breakdown of formula until they are trivially true. From the top down it is the combination of simpler facts into more complicated ones.

It’s all a very funny shell game. Somehow proofs take small steps that each feel so simple that they aren’t doing anything and build up a statement that is non obvious.


Prolog is neat. Here I’m using Tau Prolog, which a prolog that is written in Javascript. Prolog is roughly what you get when you add search and unification as primitive constructs in a language.

Prolog has multiple readings, which makes it pretty special. In one reading Prolog formula are themselves statements of axioms of a particular form (Horn clauses) that lends itself to a simple proof procedure. It also has a fairly declarative reading as a nondeterminstic match statement that tries each match in turn. Another interesting one is to consider :- to be the horizontal bar of an inference rule.

One model of the state of a prolog execution is as a sequent. The trace of prolog execution is is a sequent style proof. See Nadathur and Miller or Frank Pfenning’s notes for more

Notable tricks from the Jens Otten tutorial (which I highly recommend):

  1. Invertible rules. Rules that are reversible (in what sense?) can be eagerly applied. Use cuts !
  2. Using prolog variables and copy_term. Prolog variables may not work for higher order logic, but they do work for first order, since we’re never substituting a bound variable inside another. Prolog variables are a different face . The trick to Keep some terms around is to include a Freevar list in copy term.
  3. Skolemization
  4. Iterative deepening. No surprise here. This is a pretty standard way of making prolog search complete.

For more on these tricks, it is worthwhile to examine the leanTAP paper

There is a little bit of glue code in javascript to call the Tau Prolog solver. I used HTML textarea as input elements and sort of willy nilly grabbed from them.

function simple_query(file, query, cb) {

    var session = pl.create(1000);
    var show = function (answer) {
        document.getElementById("output").innerHTML = session.format_answer(answer);

    session.consult(file, {
        success: function () {
            // Query
            session.query(query, {
                success: function (goal) {
                    // Answers
                        success: function (answer) { show(answer); cb(answer); },
                        error: show,
                        fail: function () {
                            document.getElementById("output").innerHTML = "failure";/* Fail */
                        limit: function () { /* Limit exceeded */ console.log("limit exceeded") }
                error: show
        error: show

function prove() {
    var query = document.getElementById("querybox").value;
        query, answer => {
            document.getElementById("sequent").innerHTML = `$$\\begin{prooftree}${pretty_proof(answer.links.Proof)}

The Pretty Printer

The pretty printer is straightforward and a little janky. I am using the bussproofs package that is included in mathjax to write out my proofs trees nice.

Bussproofs flatten the tree as a post order traversal, meaning you write a node after all it’s children have been visited. It is most easily seen by examining this example. You can read more here


\(\begin{prooftree} \AxiomC{A} \UnaryInfC{B} \AxiomC{C} \BinaryInfC{D} \AxiomC{E} \AxiomC{F} \BinaryInfC{G} \UnaryInfC{H} \BinaryInfC{J} \end{prooftree}\)

Traversing through returned Tau Prolog objects is pretty straightforward. There are id fields that hold the name of the functor and args is an array holds the children. I figured it out via judicious use console.log as Tau Prolog doesn’t have the most documentation I’ve ever seen.

function pretty_formula(formula) {
    if ( == "~") {
        return `\\neg ${pretty_formula(formula.args[0])}`;
    var op = null;
    switch ( {
        case "&":
            op = "\\land"
        case "|":
            op = "\\lor"
        case "=>":
            op = "\\implies"

    if (op != null) {
        return `${pretty_formula(formula.args[0])} ${op} ${pretty_formula(formula.args[1])}`;

    return formula.toJavaScript();

function pretty_list(l) {
    switch ( {
        case ".":
            if (l.args[1].id == "[]") {
                return `${pretty_formula(l.args[0])}`;
            return `${pretty_formula(l.args[0])} , ${pretty_list(l.args[1])}`;
        case "[]":
            return "";


function pretty_sequent(seq) {
    var hyps = seq.args[0];
    var concs = seq.args[1];
    return `${pretty_list(hyps)} \\vdash ${pretty_list(concs)}`

function pretty_proof(proof) {
    if ( == "ax") {
        return `\\RightLabel{$ax$} \\AxiomC{} \\UnaryInfC{$ ${pretty_sequent(proof.args[0])} $}`;
    // Unary rules
    var label = null;
    switch ( {
        case "rimpl":
            label = "R\\implies";
        case "land":
            label = "L \\land";
        case "ror":
            label = "R \\lor"
        case "lneg":
            label = "L \\neg"
        case "rneg":
            label = "R \\neg"
    if (label != null) {
        return `${pretty_proof(proof.args[1])}
                     \\RightLabel{$ ${label} $} \\UnaryInfC{ $ ${pretty_sequent(proof.args[0])} $ }`;
    // Binary Rules
    var label = null;
    switch ( {
        case "rand":
            label = "R \\land";
        case "lor":
            label = "L \\lor";
        case "limp":
            label = "L \\implies"
    if (label != null) {
        return `${pretty_proof(proof.args[1])}
                     \\RightLabel{$ ${label} $} \\BinaryInfC{ $ ${pretty_sequent(proof.args[0])} $ }`;

You can also look at the source of this page to see everything in context. It’s just all slammed together.

Bits and Bobbles