The expressiveness of first order predicate calculus (FOPC) has led many people to use it as a representation language within computer systems. Intensive research over recent years has produced a number of efficient theorem proving techniques for FOPC, but they are all clearly subject to the limiting result that FOPC is in general semi- decidable. This paper presents a technique for investigating the decidability of particular theories of FOPC with respect to a particular theorem prover. Armed with this technique, we can frequently show that specific problems are decidable, in which case we can afford to investigate our queries for both proofs and disproofs.
This paper is not available online