Proof Methods in an Agenda-Based Natural-Deduction Theorem Prover

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 2

Theorem Proving

This note describes several methods of finding proofs used in APRVR, an agenda-based, natural-deduction theorem prover. APRVR retains a complete tree of all pending or completed goals and is able to choose the next goal to be processed from an agenda of pending goals. Through this mechanism some proof methods can be utilized that had been unavailable to an earlier prover that was not agenda-based. One approach allows information discovered in one path in an attempted proof to trigger a case split in another part of the attempted proof (NONLOCAL CASE SPLIT). Another procedure enables better handling of splitting a conjunction (AND-SPLIT) by making it possible to use more information in determining which conjunct should be split off first.