An Evaluation and Comparison of ATP systems for a First Order Spatial Theory

📄 Project Abstract

For any theory in First order Logic, it is important to show that its axiom set1 is consistent, and that its theorems follow logically from this axiom set. For anything other than the simplest of theories, proving theorems from an axiom set is no trivial matter. Often, to do so manually would be unrealistic, and so we rely on ATP (Automated Theorem Proving) systems2 to provide an automated approach to this task. However, even with the use of ATP systems, proving a set of theorems from a relatively large axiom set is still a difficult task. This is mentioned by Shyamanta Hazarika[1] as he describes the process of trying to find proofs for his own theorems, using an ATP system, SPASS. He informs us that "even seemingly simple deductions (sought within the complete axiom set) would often exhaust the available resources." It was later shown that the exhaustion of resources in this case was due to limitations of the ATP system (or the computer) itself, and in turn that, if only we could imp...