The goal of my project was to implement a simple resolution based theorem prover for first order logic in the Wolfram Language.

Conversion to Conjunctive Normal Form

In order to be able to apply the resolution method to an arbitrary sentence in first order logic, one must first convert it to conjunctive normal form (CNF). This involves two crucial steps, conversion to prenex normal form (PNF) and Skolemization

I started my project by implementing the conversion to prenex normal form. The example bellow illustrates the implemented functionality,

formula = ForAll[x,Implies[ForAll[y,Implies[animal[y],loves[x,y]]],Exists[z,loves[z,x]]]]
prenexForm[formula]

$$ \forall _x\left(\forall _y(\text{animal}(y)\Rightarrow \text{loves}(x,y))\Rightarrow \exists _z\text{loves}(z,x)\right) $$

$$ \forall _{x_0}\exists _{y_1}\exists _{z_2}\left(\neg \left(\neg \text{animal}\left(y_1\right)\lor \text{loves}\left(x_0,y_1\right)\right)\lor \text{loves}\left(z_2,x_0\right)\right) $$

Next, in order to eliminate existential quantifiers and obtain equisatisfiable formula, based on Hector Zenil's demonstration [1.] I created a function for Skolemization.

skolemize[prenexForm[formula]]

$$ \forall _{x_0}\left(\neg \left(\neg \text{animal}\left(f_2\left(x_0\right)\right)\lor \text{loves}\left(x_0,f_2\left(x_0\right)\right)\right)\lor \text{loves}\left(f_1\left(x_0\right),x_0\right)\right) $$

Now by using Mathematicas's BooleanConver[] on the matrix of the formula we obtain a CNF of the original formula. $$ \forall_{x_0} \left(\text{animal}\left(f_2\left(x_0\right)\right)\lor \text{loves}\left(f_1\left(x_0\right),x_0\right)\right)\land \left(\neg \text{loves}\left(x_0,f_2\left(x_0\right)\right)\lor \text{loves}\left(f_1\left(x_0\right),x_0\right)\right) $$

Most General Unification

Afterwards, I implemented the most general unification (MGU) algorithm, which is a central part of a resolution based theorem prover. Given two first order terms, the unify function returns the minimal substitution of terms for variables, such that the terms become identical after the substitution is applied. Consider the following example,

formula1 = f[x, g[a], g[z]];
formula2 = f[g[y], g[y], g[g[x]]] ;
unify[formula1 , f2]

Returns the following substitution $\sigma = \{x\to g(a),y\to a,z\to g(g(a))\}$ . Notice that after applying $\sigma$ to $\text{formula}_1$ and $\text{formula}_2$ they become the same formula.

Resolution

Having all the components in place I implemented the resolution and factoring algorithms using two resolution strategies, Set of Support and Linear Resolution, thereby completing the implementation of the theorem prover. In order to prove a given theorem form a given set of axioms, we provide the theorem prover with a negation of the theorem and the prover will apply resolution looking for a contradiction. If the original theorem was entailed by the axioms the contradiction will be found.

In the bellow examples it is important to know that the theorem prover represents a disjunction of A and B as {A, B}

Binary Resolution principle:

resolve[{!Animal[f[Jack[]]],Loves[g[Jack[]],Jack[]] },{Animal[f[x]],Loves[g[x],x]}]

Factoring:

resolveAndFactor[{! Animal[f[Jack[]]], 
  Loves[g[Jack[]], Jack[]] }, {Animal[f[x]], Loves[g[x], x]}]

The resulting implementation provides a complete semi-decision procedure for first order logic. In principle given infinite time and memory the theorem prover could find a proof of any theorem (in first order logic) entailed by a given set of axioms.

Example Proofs

Now we shall explore some examples of automatically generated proofs,

A Simple Mathematical Example

Given that $$f(x,y) = f(y,x) $$ the prover shows that $$f(f(a,b), f(c,d)) = f(f(d,c),f(b,a))$$

thm = {!eq[f[f[a[],b[]],f[c[],d[]]], f[f[d[],c[]],f[b[],a[]]]]};
axioms ={
         {eq[x,x]},
         {!eq[y,z], eq[z,y]},
         {!eq[p,q], !eq[q,r], eq[p,r]},
         {eq[f[i,j], f[j,i]]},
         {!eq[n,m],!eq[k,l],eq[f[n,k],f[m,l]]}
       };
linearResolution[thm, axioms, 5]

A Simple Story Example

Consider the following problem:

The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American

We shall translate it to first order logic and then use the resolution prover to show that Colonel West is a Criminal.

thm2 = {!Criminal[West[]]};
axioms2 = {{!American[x],!Weapon[y],!Sells[x,y,z],!Hostile[z],Criminal[x]},
       {!Missile[w], !Owns[Nono[],w], Sells[West[],w,Nono[]]},
       {!Enemy[q,America[]],Hostile[q]},
       {!Missile[r],Weapon[r]},
       {Owns[Nono[], Rocket[]]},
       {American[West[]]},
       {Missile[Rocket[]]},
       {Enemy[Nono[], America[]]}
};
linearResolution[thm2, axioms2, 8]

It is worth noticing that this deduction although intuitively obvious for humans, requires many steps to be proven by the computer.

Conclusions and Further work

Although resolution provides a refutation-complete method for theorem proving, the time required to prove complicated theorems would be extremely high due to a combinatorial explosion of the search space. In order to be able to prove such results one must restrict the search space and remove redundancies by applying optimizations and heuristics on top of the pure resolution method.

Some of the logical improvements would include implementation of subsumption, tautology deletion, Knuth - Bendix ordering, paramodulation and unit preference. These could drastically improve the performance of the theorem prover.

References:

1. H. Zenil, http://demonstrations.wolfram.com/Skolemization/
2. J. A. Robinson, A. Voronkov, Handbook of Automated Reasoning
3. P. Norvig, S. J. Russell, Artificial Intelligence: A Modern Approach
4. C. L. Chang, R. C. T. Lee, Symbolic Logic and Mechanical Theorem Proving