Automatic Theorem Proving

Origin. Soviet work in mathematical logic and automatic reasoning; contributions by Maslov (inverse method, 1964), Lifschitz, and others; connections to the Soviet tradition in mathematical logic from Kolmogorov and Markov.

Mechanism. Proves theorems by systematic search through the space of possible proofs. The inverse method (Maslov) works bottom-up, starting from axioms and deriving consequences until the goal is reached, in contrast to resolution's top-down refutation. Soviet work emphasized decidable fragments, proof complexity, and connections between proof-theoretic and model-theoretic methods.

Procedure. Formalize the domain as axioms in first-order logic. State the theorem to prove. Apply the inference method: resolution builds a refutation tree seeking contradiction; the inverse method builds a proof tree seeking the goal. Use heuristics to guide search: prefer shorter clauses, prefer clauses that unify with the goal, prune subsumed clauses. If a proof is found, extract it; if the search space is exhausted, the theorem does not follow from the axioms.

Applies to. Verification, mathematics, any domain where correctness can be expressed as logical entailment.

Limitations. Combinatorial explosion: the search space grows exponentially with formula complexity. Heuristics help but do not eliminate the fundamental hardness. Also: formalization is the bottleneck — translating an informal claim into precise logic often reveals ambiguities and missing assumptions. The proof may be correct but the formalization wrong.