An Incremental Theorem Prover
Proceedings of the Tenth International Joint Conference on Artificial Intelligence. Reasoning. 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 .
@inproceedings{ijcai1987p203,
title = {An Incremental Theorem Prover},
author = {Shanahan, Murray},
booktitle = {Proceedings of the Tenth International Joint Conference on
Artificial Intelligence, {IJCAI-87}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {John McDermott},
pages = {987--988},
year = {1987},
note = {Reasoning},
url = {https://ijcai.org/proceedings/1987/203},
}
TY - CPAPER TI - An Incremental Theorem Prover AU - Shanahan, Murray T2 - Proceedings of the Tenth International Joint Conference on Artificial Intelligence, IJCAI-87 PB - International Joint Conferences on Artificial Intelligence PY - 1987 SP - 987 EP - 988 UR - https://ijcai.org/proceedings/1987/203 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
