Automated Theorem-Proving and Axiomatic Mathematics

Jonathan Gorard, Wolfram Research / Cambridge University

ABSTRACT

This talk will be a brief introduction to the current status of the Wolfram Language’s framework for automated theorem-proving and axiomatic representation of pure mathematics, as of Version 12. This includes recent updates to the FindEquationalProof function, and the newly-introduced AxiomaticTheory function. The talk will explain some of the basic algorithmic principles behind the theorem-proving framework, such as Knuth-Bendix (unfailing) completion and superposition calculus, and will also briefly demonstrate some future planned functionality (including support for higher-order logics, temporal logic, modal logic, etc.)

What is Automated Theorem-Proving?

Pure mathematicians are abstract machines for converting assumptions and conjectures into theorems and proofs.

Can we develop an algorithm which accepts a theorem and a set of axioms as input, and returns a formal mathematical proof as output?

Is this even possible?

Gödel’s incompleteness theorems, Tarski’s undefinability theorem, Turing’s proof of undecidability for the halting problem, undecidability of Hilbert’s Entscheidungsproblem, etc.

Proofs should be human-readable (informal), but also computable (formal).

Ultimately, we need to curate a large corpus of mathematical knowledge, and also develop a semantic language for representing mathematical concepts in the Wolfram Language.

Equational Logic Theorems

FindEquationalProof[thm,axms]

Attempts to find a proof of the equational logic theorem thm, using the axioms axms. For instance:

proof=FindEquationalProof[a==c,{a==b,b==c}]

proof["ProofGraph"]

groupTheory={ForAll[{a,b,c},g[a,g[b,c]]==g[g[a,b],c]],ForAll[a,g[a,e]==a],ForAll[a,g[a,inv[a]]==e]};
proof2=FindEquationalProof[ForAll[x,g[e,x]==x],groupTheory]

proof2["ProofDataset"]/.g->CenterDot

proof2["ProofNotebook"]/.g->CenterDot

proof2["ProofFunction"]

%[]

FindEquationalProof[ForAll[{a,b,c,d},g[a,inv[g[b,g[g[g[c,inv[c]],inv[g[d,b]]],a]]]]==d],groupTheory]

%["ProofGraph"]

shortLogic={ForAll[{a,b},nand[nand[a,a],nand[a,b]]==a],ForAll[{a,b},nand[a,nand[a,b]]==nand[a,nand[b,b]]],ForAll[{a,b,c},nand[a,nand[a,nand[b,c]]]==nand[b,nand[b,nand[a,c]]]]};
wolframLogic=ForAll[{a,b,c},nand[nand[nand[a,b],c],nand[a,nand[nand[a,c],a]]]==c];
proof3=FindEquationalProof[shortLogic,wolframLogic]

proof3["ProofGraph"]

Proofs are represented using the ProofObject structure. FindEquationalProof returns a proof of an equational theorem, if and only if FullSimplify evaluates to True for that theorem.

Internally, FindEquationalProof implements the Knuth-Bendix unfailing uncompletion algorithm from universal algebra.

Axiomatic Representations

AxiomaticTheory["theory"]

Returns the standard axiomatic representation for the (equational) theory "theory". For instance:

AxiomaticTheory["BooleanAxioms"]

AxiomaticTheory["GroupAxioms"]

AxiomaticTheory["GroupAxioms","Supertheories"]

AxiomaticTheory["AbelianGroupAxioms"]

AxiomaticTheory["GroupAxioms","Operators"]

AxiomaticTheory[{"GroupAxioms",<|"Multiplication"->g,"Inverse"->inv,"Identity"->e|>}]

AxiomaticTheory["GroupAxioms","NotableTheorems"]

AxiomaticTheory[{"GroupAxioms",<|"Multiplication"->g,"Inverse"->inv,"Identity"->e|>},"NotableTheorems"]

FindEquationalProof[AxiomaticTheory[{"GroupAxioms",<|"Multiplication"->g,"Inverse"->inv,"Identity"->e|>},"NotableTheorems"]["InverseOfComposite"],AxiomaticTheory[{"GroupAxioms",<|"Multiplication"->g,"Inverse"->inv,"Identity"->e|>}]]

%["ProofGraph"]

AxiomaticTheory[{"theory",ops}], where ops is an association, allows one to override the default choice of operators for the given theory.

Internally, AxiomaticTheory has a similar structure to an EntityStore.

Defining (e.g. Arithmetic) Operators

Proving theorems involving predefined symbols (such as arithmetic operators) can be tricky, because the front-end will automatically evaluate things to True:

FindEquationalProof[ForAll[x,-(-x)==x],{}]

ForAll[x,-(-x)==x]

However, we can easily define our own arithmetic operators, and typeset them as we wish:

proof=FindEquationalProof[ForAll[x,minus[minus[x]]==x],{ForAll[x,plus[x,0]==x],ForAll[x,plus[x,minus[x]]==0],ForAll[{a,b,c},plus[a,plus[b,c]]==plus[plus[a,b],c]]}]

proof["ProofDataset"]

proof["ProofDataset"]/.{minus->OverTilde,plus->CirclePlus}

What is a Proof?

An axiom can be thought of as being equivalent to a pair of symbolic rewrite rules: x==y is equivalent to the pair {x_->y,y_->x}.

A theorem can also be represented as a statement that two symbolic expressions are equivalent.

A proof is therefore just a particular sequence of symbolic (axiomatic) transformations which transforms one symbolic expression into another.

Why is Theorem-Proving Hard?

Theorem-proving is hard in general, because symbolic rewrite systems tend not to be confluent (i.e. they do not exhibit the Church-Rosser property of the lambda calculus).

Newman’s Lemma: a (strongly normalizing) symbolic rewrite system is confluent if and only if every critical pair converges.

Therefore, if we can compute all critical pairs, and add them as equational lemmas to the rewrite system, we can thereby force the system to be confluent (Knuth-Bendix completion).

A Glimpse of the Future

These functions are not yet part of the Wolfram Language, but are planned for release in versions 12.1 and beyond.

Generating Counterexamples

Proving theorems is a proof-theoretic problem, but finding counterexamples is a model-theoretic problem:

FindEquationalProof[a==c,a==b]

FindEquationalProof[ForAll[x,g[x,e]==e],{ForAll[{x,y,z},g[x,g[y,z]]==g[g[x,y],z]],ForAll[x,g[e,x]==x],ForAll[x,g[inv[x],x]==e]}]

counterexample=FindEquationalCounterexample[ForAll[x,g[x,e]==e],{ForAll[{x,y,z},g[x,g[y,z]]==g[g[x,y],z]],ForAll[x,g[e,x]==x],ForAll[x,g[inv[x],x]==e]}]

counterexample["CounterexampleAssociation"]

counterexample["FalsificationFunction"]

%[]

Predicate (First-Order) Logic

Using skolemization, superposition calculus, and other algorithmic concepts, we can reduce expressions in first-order logic to equisatisfiable expressions in equational logic:

proof=FindEquationalProof[Mortal[Socrates],{ForAll[x,Implies[Man[x],Mortal[x]]],Man[Socrates]}]

proof["ProofGraph"]

proof["ProofDataset"]

proof2=FindEquationalProof[Exists[x,Mortal[x]],{ForAll[x,Implies[Man[x],Mortal[x]]],Exists[x,Man[x]]}]

proof2["ProofGraph"]

proof3=FindEquationalProof[Not[Exists[x,And[Baby[x],ManageCrocodile[x]]]],{ForAll[x,Implies[Baby[x],Not[Logical[x]]]],ForAll[x,Implies[ManageCrocodile[x],Not[Despised[x]]]],ForAll[x,Implies[Not[Logical[x]],Despised[x]]]}]

proof3["ProofGraph"]

proof4=FindEquationalProof[And[Knight[Zoey],Knave[Mel]],{ForAll[p,ForAll[s,Implies[And[Knight[p],Says[p,s]],s]]],ForAll[p,ForAll[s,Implies[And[Knave[p],Says[p,s]],Not[s]]]],ForAll[p,Or[Knight[p],Knave[p]]],Says[Zoey,Knave[Mel]],Says[Mel,And[Not[Knave[Zoey]],Not[Knave[Mel]]]]}]

proof4["ProofGraph"]