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) {
console.log(
);
};

session.consult(file, {
success: function () {
// Query
session.query(query, {
success: function (goal) {
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,
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.