非表示:
キーワード:
-
要旨:
We extend previous results about resolution and superposition with ordering \u000Aconstraints and selection functions to the case of general (quantifier‐free) \u000Afirst‐order formulas with equality. The refutation completeness of our calculi \u000Ais compatible with a general and powerful redundancy criterion which includes \u000Amost (if not all) techniques for simplifying and deleting formulas. The \u000Aspectrum of first‐order theorem proving techniques covered by our results \u000Aincludes ordered resolution, positive resolution, hyper‐resolution, semantic \u000Aresolution, set‐of‐support resolution, and Knuth/Bendix completion, as well as \u000Atheir extension to general first‐order formulas. An additional feature in the \u000Alatter case is our efficient handling of equivalences as equalities on the \u000Alevel of formulas. Furthermore, our approach applies to constraint theorem \u000Aproving, including constrained resolution and theory resolution.
