Notes on Automated Theorem Proving, Part 1 - Propositional Logic

by Alex Nelson, 15 January 2015

Introduction. I will be starting a series on my endeavor to implement an automated theorem prover. In this article, we will implement an automated theorem prover for classical propositional logic. In the next article we will begin exploring first-order (“predicate”) logic, again classical.

If the reader does not know propositional logic, I strongly urge the reader to consult Elliot Mendelson’s Introduction to Mathematical Logic (or something similar) for details…because I will give a comical overview of the bare bones necessary to ask questions. No pretension of completeness here!

All the code is available on github, checkout v0.0.2 for the code relevant to this post.

1. Overview of Propositional Logic. We have some formula, built up from propositional variables and logical operators (“and”, “or”, “not”, etc.). We have some valuations, which evaluate the propositional formula as either true or false. (Think of a valuation as picking one particular row of a truth table.)

A propositional formula is said to be a “Tautology” or Valid if it is always true in every valuation (for example “A or not A”, we have two possible valuations: (i) A is false, in which case the proposition evaluates to “false or true”, i.e., true; (ii) A is true, in which case the proposition evaluates to “true or false”, i.e., true).

A propositional formula is said to be “Satisfiable” if there is at least one valuation which makes it true.

A propositional formula is said to be “Unsatisfiable” (or a Contradiction) if there are no valuations which make it true.

The basic questions we ask ourselves is “Given a propositional formula, is it a tautology? Is it satisfiable? Is it unsatisfiable?”

The challenge here is, the naive way to answer “A formula is a tautology” is to check all possible valuations. If there are n propositional variables in the formula, that’s 2^n possible valuations. We have an NP-Complete Problem!

Remark. Observe that a formula f is satisfiable if and only if f is not unsatisfiable.

Also, a formula f is a tautology if and only if not f is unsatisfiable.

Although all tautologies are satisfiable formulas, not all satisfiable formulas are tautologies…just as all trout are fish, but not all fish are trout. (End of Remark)

A Vanilla Automated Theorem Prover for Propositional Logic

2. Abstract Syntax Tree. The basic data structure we’ll work with is a Formula, which is either true T, false F, a propositional variable, or something involving a logical operator among formulas. A propositional variable is represented as PropVar just an alias for a string.

type PropVar = String --- Proposition variables are strings

data Formula = F
             | T
             | Atom PropVar
             | Not Formula
             | And Formula Formula
             | Or Formula Formula
             | Implies Formula Formula
             | Iff Formula Formula
               deriving (Show, Eq)

When we get to first-order logic, we will extend this to include quantifiers.

Remark. If someone were curious what sort of syntax we should be supporting, I would think the TPTP syntax would be best. But since that would distract us too much from the interesting problem, so we leave it as an exercise for the reader ;) (End of Remark)

(Addendum: This actually embodies more truth about the structure of “real” theorem provers than I first realize. Usually there are multiple modules/standalone-programs which transform the problem. A syntactic reader/printer is one of these components. But we’re interested in the engine not the paint job.)

3. Valuations. We need valuations, that is, functions which evaluate an PropVar to be either True or False. So we just create an alias:

type Valuation = PropVar -> Bool

We will be modifying this in first-order logic to work with terms, but for now evaluating a propositional variable is all we need.

3.1. Getting All Atoms. So, we’re going to have to exhaustively search all atoms. We need a function atoms which will (i) eat in a formula, and (ii) produce a list of the atoms in the formula without duplicates. We have

rawAtoms :: Formula -> [PropVar]
rawAtoms f = case f of
  F           -> []
  T           -> []
  Atom x      -> [x]
  Not p       -> rawAtoms p
  And p q     -> (rawAtoms p) ++ (rawAtoms q)
  Or p q      -> (rawAtoms p) ++ (rawAtoms q)
  Implies p q -> (rawAtoms p) ++ (rawAtoms q)
  Iff p q     -> (rawAtoms p) ++ (rawAtoms q)

--- import qualified Data.List as Data.List
atoms :: Formula -> [PropVar]
atoms = Data.List.nub . rawAtoms

4. Semantics. Now we come to the bread and butter of this thing: the eval function. We should evaluate a Formula specifically in the context of a Valuation, and return True or False. This is done recursively, exploring the arguments to the various logical operations “in the obvious way”:

eval :: Formula -> Valuation -> Bool
eval f v = case f of
  F           -> False
  T           -> True
  Atom x      -> v x
  Not p       -> not (eval p v)
  And p q     -> (eval p v) && (eval q v)
  Or p q      -> (eval p v) || (eval q v)
  Implies p q -> not (eval p v) || (eval q v)
  Iff p q     -> (eval p v) == (eval q v)

5. The Main Player. We now almost have enough to begin asking whether a function is a tautology or not (or satisfiable, or not). We first introduce a function which exhaustively checks all valuations. It takes in a subfn (which for us is just eval fm curried), a valuation it resorts to v when all else fails, and a set of atoms ats.

This function recursively calls itself, popping one atom at a time, and considering both the case the popped atom is true…and when it is false. When its all out of atoms, it begins to call the subfn on the given valuation v.

onAllValuations :: (Valuation -> Bool) -> Valuation -> [PropVar] -> Bool
onAllValuations subfn v ats = case ats of
  []   -> subfn v
  p:ps -> let v' t q = if q == p then t else v q in
          (onAllValuations subfn (v' False) ps)
          && (onAllValuations subfn (v' True) ps)

Great, now we can begin asking if something is a tautology or not. That amounts to asking if onAllValuations (eval fm) is True for an arbitrary initial valuation (so why not pick (const False)?) on all the atoms in the formula.

Unsatisfiability is simply the case the negation of a given formula is a tautology. Satisfiability is when a formula is not unsatisfiable.

isTautology :: Formula -> Bool
isTautology fm = onAllValuations (eval fm) (const False) (atoms fm)

isUnsatisfiable :: Formula -> Bool
isUnsatisfiable fm = isTautology (Not fm)

isSatisfiable :: Formula -> Bool
isSatisfiable fm = not (isUnsatisfiable fm)

This is a horribly inefficient way to implement satisfiability, I think. Why? Well, it depends on the formula. There are a lot of tricks to transform the formula to put it in some canonical form. Transforming the formula into a logically equivalent one turns out to improve performance quite a bit.

Conclusion

We’ve got the moving parts for the automated theorem prover done. All that’s left is to write a parser (not relevant at the moment), and perhaps some REPL-type code for interactive sessions.

But the code is horribly inefficient. Next time, we will consider various different canonical forms for the propositional formulas to increase performance.

References

  1. Laurence Edward Day, “Implementing a Propositional Logic Theorem Prover in Haskell”. Undergraduate dissertation (2010) eprint
  2. John Harrison, Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
  3. Elliot Mendelson, Introduction to Mathematical Logic. Chapman and Hall, 5th ed., 2009.
  4. Prof. Dr. Erika Ábrahám Lectures on Decision Procedures, specifically propositional logic satisfiability.