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 http://jens-otten.de/tutorial_cade19/ 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

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 https://formal.iti.kit.edu/beckert/leantap/.

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);
        console.log(
            session.format_answer(answer)
        );
    };

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

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

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. http://docs.mathjax.org/en/latest/input/tex/extensions/bussproofs.html?highlight=bussproofs

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 https://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/BussGuide2_Smith2012.pdf.

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

\(\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 (formula.id == "~") {
        return `\\neg ${pretty_formula(formula.args[0])}`;
    }
    var op = null;
    switch (formula.id) {
        case "&":
            op = "\\land"
            break;
        case "|":
            op = "\\lor"
            break;
        case "=>":
            op = "\\implies"
            break;

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

    return formula.toJavaScript();
}

function pretty_list(l) {
    switch (l.id) {
        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 (proof.id == "ax") {
        return `\\RightLabel{$ax$} \\AxiomC{} \\UnaryInfC{$ ${pretty_sequent(proof.args[0])} $}`;
    }
    // Unary rules
    var label = null;
    switch (proof.id) {
        case "rimpl":
            label = "R\\implies";
            break;
        case "land":
            label = "L \\land";
            break;
        case "ror":
            label = "R \\lor"
            break;
        case "lneg":
            label = "L \\neg"
            break;
        case "rneg":
            label = "R \\neg"
            break;
    }
    if (label != null) {
        return `${pretty_proof(proof.args[1])}
                     \\RightLabel{$ ${label} $} \\UnaryInfC{ $ ${pretty_sequent(proof.args[0])} $ }`;
    }
    // Binary Rules
    var label = null;
    switch (proof.id) {
        case "rand":
            label = "R \\land";
            break;
        case "lor":
            label = "L \\lor";
            break;
        case "limp":
            label = "L \\implies"
            break;
    }
    if (label != null) {
        return `${pretty_proof(proof.args[1])}
                   ${pretty_proof(proof.args[2])}
                     \\RightLabel{$ ${label} $} \\BinaryInfC{ $ ${pretty_sequent(proof.args[0])} $ }`;
    }
}

You can also look at the source of this page to see everything in context. https://raw.githubusercontent.com/philzook58/philzook58.github.io/master/_posts/2021-02-07-javascript-automated-proving.md It’s just all slammed together.

Bits and Bobbles