非表示:
キーワード:
-
要旨:
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.
