Automatic Theorem Proving

Origin. Soviet mathematical logic and automatic reasoning, 1960s-1980s. Key contributions by Sergei Maslov (inverse method, 1964), Vladimir Lifschitz, and others. Built on the Soviet tradition in mathematical logic from Kolmogorov and Markov. The inverse method provided an alternative to resolution-based theorem proving.

Mechanism. Theorems are proved by systematic search through the space of possible proofs. Resolution works top-down by refutation: assume the negation of the goal and derive a contradiction. Maslov's inverse method works bottom-up: start from axioms and derive consequences until the goal is reached. Soviet work emphasized decidable fragments of logic, proof complexity analysis, and connections between proof-theoretic and model-theoretic methods.

Procedure. Prove theorems automatically through systematic search: (1) Formalize the domain — express domain knowledge as axioms in first-order logic. Formalization must be precise; ambiguity in informal statements becomes explicit here. (2) State the theorem — express what is to be proved as a logical formula. The prover will attempt to derive this from the axioms. (3) Choose inference method — resolution builds a refutation tree seeking contradiction; the inverse method builds a proof tree seeking the goal directly. Each has different performance characteristics. (4) Apply search heuristics — the search space is combinatorially large. Heuristics guide exploration: prefer shorter clauses, prefer clauses that unify with the goal, prune subsumed clauses, apply domain-specific guidance. (5) Extract the proof — if a proof is found, extract it in human-readable form. The proof can be checked independently. (6) Interpret failure — if the search space is exhausted without proof, the theorem does not follow from the axioms as formalized. This may indicate the theorem is false, or that the formalization is incomplete.

Applies to. Formal verification. Mathematical proof. Hardware and software correctness. Any domain where correctness can be expressed as logical entailment from precise axioms.

Limitations. Combinatorial explosion: search space grows exponentially with formula complexity. Heuristics help but do not eliminate fundamental hardness. Formalization is the practical bottleneck — translating informal claims into precise logic reveals ambiguities and missing assumptions. The proof may be correct but the formalization wrong. First-order logic is undecidable in general; provers may run indefinitely on unprovable goals.