---
title: "An Incremental Theorem Prover"
authors:
  - "Murray Shanahan"
doi: ""
url: "https://ijcai.org/proceedings/1987/203"
pdf: "https://ijcai.org/proceedings/1987/0203.pdf"
venue: "Proceedings of the Tenth International Joint Conference on Artificial Intelligence"
year: 1987
pages: "987-988"
track: "Reasoning"
keywords:
---

# An Incremental Theorem Prover

Murray Shanahan

*Proceedings of the Tenth International Joint Conference on Artificial Intelligence*, pages 987-988.

## 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 ~earch 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 .