Theorem Prover

Theorem Prover is an OCaml desktop app that can evaluate the satisfiability of statements in first-order logic. Users can enter any statement in propositional logic in plain English, and the Prover will provide a step-by-step proof of its satisfiability.

Logic

In propositional logic, statements are represented by propositional variables such as $p$ and $q$ which represent truth values (T/F). Compound propositions are formed by logical connectives "and" ($\land$), "or" ($\lor$), and "not" ($\lnot$) as well as "implies" ($\implies$) and "if and only if" ($\iff$).

First-order logic builds off of propositional logic by adding quantified variables. There are two quantifiers: universal (for all, $\forall$) and existential (there exists, $\exists$). For instance, for a predicate $h$ that takes two variables, the statement $\forall x\ \exists y\ h(x,y)$ reads "for all x there exists y such that h(x,y)."

Resolution

Resolution is a rule of inference leading to a refutation-complete theorem proving technique for sentences in propositional logic and first-order logic. Refutation-commpleteness means that it is able to derive "false" from every unsatisfiable set of formulas. By negating the statement, we can derive "true" any statements that must hold.

The resolution rule can be summarized as $(p_1\lor q)\land (p_2\lor \neg q)\implies (p_1\lor p_2)$. This leads to a simplified clause. When coupled with a complete search algorithm, resolution allows us to determine the satisfiability of a statement.

Step 1: Negate the statement

Resolution is essentially a proof by contradiction, so we start by considering the negation of the statement.

Step 2: Convert to conjunctive normal form

To do resolution, statements must be in conjunctive normal form, i.e. a conjunction of disjunctions of literals, or "an AND of ORs". A first-order logic statement is converted to CNF as follows:

1. Convert to negation normal form.

   a) Eliminate implications and equivalences. Replace $p\implies q$ with $\neg p \lor q$ and replace $p\iff q$ with $(p\lor \neg q)\land (\neg p\lor q)$.

   b) Move NOTs inwards by applying De Morgan's law: Replace $\neg(p\lor q)$ with $\neg p\land \neg q$, replace $\neg(p\land q)$ with $\neg p\lor \neg q$, and replace $\neg\neg p$ with $p$. Replace $\neg(\forall x\ p(x))$ with $\exists x\ \neg p(x)$ and replace $\neg(\exists x\ p(x))$ with $\forall x\ \neg p(x)$.

2. Standardize variables.

   a) For sentences that use the same variable name twice, change the name of one of the variables.

3. Skolemize the statement.

   a) Move quantifiers outwards.

   b) Replace $\forall x_1\dots\forall x_n\exists y\ p(y)$ with $\forall x_1\dots\forall x_n\ p(f(x_1,\dots,x_n))$ where $y$ is represented instead as a function of the first variables $x_1,\dots,x_n$. This preserves satisfiability.

4. Drop all universal quantifiers.

5. Distribute ORs inwards over ANDs: replace $p\lor (q\land r)$ with $(p\lor q)\land (p\lor r)$.

Step 3: Apply resolution by brute force

For any two "clauses" (aka disjunctions) that make up the statement in CNF, and for any two shared variables, if they are in the form $p$ and $\neg p$, then we apply CNF to produce a new clause.

In implementation, to avoid losing information, we keep the original two clauses and add this new clause to our list of clauses. If we create an empty clause, this is a contradiction, at which point we can show that the initial statement must be true. If we do not arrive at an empty clause but cannot create additional clauses via resolution, then we can conclude that the satisfiability is unknown.