Non‐clausal Resolution and Superposition with Selection and Redundancy Criteria

Bachmair, Leo; Ganzinger, Harald

doi:10.1007/BFb0013068

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

このアイテムの新しいバージョンが利用可能です:
https://pure.mpg.de/pubman/item/item_2052720_3

詳細要約

公開

会議論文

Non‐clausal Resolution and Superposition with Selection and Redundancy Criteria

MPS-Authors

/persons/resource/persons44055

Bachmair, Leo
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44474

Ganzinger, Harald
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

公開されているフルテキストはありません

付随資料 (公開)

There is no public supplementary material available

引用

Bachmair, L., & Ganzinger, H. (1992). Non‐clausal Resolution and Superposition with Selection and Redundancy Criteria. In A., Voronkov (Ed.), Logic Programming and Automated Reasoning (pp. 273-284). Berlin: Springer.

引用: https://hdl.handle.net/11858/00-001M-0000-0023-C430-0

要旨

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.