An Incremental Theorem Prover

Abstract

When states of affairs are represented by theories, reasoning about them often involves making a small change to a set of axioms, and computing the consequences of that change for the set of theorems derivable from those axioms. A Prolog-like theorem prover is described which, as it explores the space of possible proofs for a set of formulae, records the structure of that space. This information can be used to search efficiently for proofs for the same formulae with a slightly changed set of axioms. Existing Prolog interpreters throw away all such information, so that the entire space of possible proofs for each formula must be explored from scratch every time the set of axioms is changed, no matter how little that change affects the search space's structure.