New Directions in Instantiation-Based Theorem Proving

We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation