📐 Theorem Prover

Automated propositional logic prover with proof search, NNF, and truth tables

Overview

This module implements an automated theorem prover for propositional logic. Given a formula, it can determine whether it's a tautology, find a constructive proof via sequent-calculus-style backward search, verify entailment from assumptions, and generate truth tables — all from scratch in pure OCaml.

The prover uses fuel-bounded search to guarantee termination while exploring deep proof trees.

Formula Language

type formula =
  | Atom of string                 (* propositional variable: "P", "Q" *)
  | Not of formula                 (* ¬φ *)
  | And of formula * formula       (* φ ∧ ψ *)
  | Or of formula * formula        (* φ ∨ ψ *)
  | Implies of formula * formula   (* φ → ψ *)
  | Iff of formula * formula       (* φ ↔ ψ *)
  | True | False                   (* constants *)

(* Parser included: "P -> (Q & R)" parses to Implies(Atom "P", And(Atom "Q", Atom "R")) *)
let parse s = ... (* tokenizer + recursive descent *)

Proof Search

The core algorithm works by backward proof search on sequents (context ⊢ goal). It applies logical rules to decompose the goal until it matches an axiom (goal found in context) or runs out of fuel:

type rule_name =
  | Axiom           (* goal ∈ context *)
  | TrueIntro       (* ⊢ True always *)
  | FalseElim       (* False ∈ context ⊢ anything *)
  | AndIntro        (* prove both conjuncts *)
  | AndElimL | AndElimR  (* decompose And in context *)
  | OrIntroL | OrIntroR  (* pick a disjunct to prove *)
  | OrElim          (* case split on Or in context *)
  | ImpliesIntro    (* assume antecedent, prove consequent *)
  | ImpliesElim     (* modus ponens from context *)
  | NotIntro        (* assume φ, derive contradiction *)
  | NotElim         (* from ¬¬φ derive φ *)
  | IffIntro | IffElim  (* bidirectional implication *)

(* Each rule produces sub-goals; search recurses with decremented fuel *)
let prove_sequent ?(fuel=50) ctx goal = ...

Proof Objects

type proof = {
  rule    : rule_name;
  sequent : context * formula;  (* what was proved *)
  children: proof list;         (* sub-proofs *)
}

(* Proofs can be inspected for size, depth, and which rules were used *)
let rec proof_size p = 1 + List.fold_left (fun s c -> s + proof_size c) 0 p.children
let rec proof_depth p = 1 + List.fold_left (fun d c -> max d (proof_depth c)) 0 p.children
let rules_used proof = ... (* collect all rule names in the proof tree *)

Additional Features

Feature	Description
Negation Normal Form	`nnf` pushes negations inward, eliminating double negation and Implies/Iff
Substitution	`subst name replacement f` replaces atoms in a formula
Truth Table	`truth_table f` enumerates all variable assignments, evaluating the formula under each
Truth Table Tautology	Brute-force verification by checking all rows — useful as a cross-check against proof search
Entailment	`entails assumptions goal` checks if the assumptions logically imply the goal
Complexity Metric	`complexity f` counts connectives — a rough measure of formula difficulty
Pretty Printer	Precedence-aware formatter with minimal parenthesization

Example Session

(* Is "P → P" a tautology? *)
# is_tautology (Implies (Atom "P", Atom "P"));;
- : bool = true

(* Prove it constructively: *)
# prove (Implies (Atom "P", Atom "P"));;
- : proof option = Some {
    rule = ImpliesIntro;
    sequent = ({P}, P);
    children = [{rule = Axiom; sequent = ({P}, P); children = []}]
  }

(* De Morgan's law: ¬(P ∧ Q) ↔ (¬P ∨ ¬Q) *)
# is_tautology (parse "~(P & Q) <-> (~P | ~Q)");;
- : bool = true

(* Entailment: does {P → Q, Q → R} ⊢ P → R? *)
# entails [parse "P -> Q"; parse "Q -> R"] (parse "P -> R");;
- : bool = true

OCaml Concepts Demonstrated

Recursive algebraic types — formula is a tree of connectives, naturally modeled as a variant
Set.Make functor — FormulaSet gives ordered sets of formulas for contexts
Recursive descent parsing — tokenizer + parser with operator precedence
Optional return types — prove returns proof option (Some on success, None if unprovable within fuel)
Fuel-bounded recursion — decreasing integer parameter guarantees termination
Higher-order evaluation — eval env f takes a variable assignment as an environment

Running It

# Compile and run
ocamlfind ocamlopt -package str -linkpkg theorem_prover.ml -o theorem_prover
./theorem_prover

# Runs demonstrations of tautology checking, proof search,
# truth tables, NNF conversion, and entailment