Associative-commutative superposition

Bachmair, Leo; Ganzinger, Harald

アイテム詳細

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

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

報告書

Associative-commutative superposition

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.

フルテキスト (公開)

MPI-I-93-267.pdf
(全文テキスト（全般）), 123KB

付随資料 (公開)

There is no public supplementary material available

引用

Bachmair, L., & Ganzinger, H.(1993). Associative-commutative superposition (MPI-I-93-267). Saarbrücken: Max-Planck-Institut für Informatik.

引用: https://hdl.handle.net/11858/00-001M-0000-0014-B4F9-9

要旨

We present an associative-commutative paramodulation calculus that generalizes the associative-commutative completion procedure to first-order clauses. The calculus is parametrized by a selection function (on negative literals) and a well-founded ordering on terms. It is compatible with an abstract notion of redundancy that covers such simplification techniques as tautology deletion, subsumption, and simplification by (associative-commutative) rewriting. The proof of refutational completeness of the calculus is comparatively simple, and the techniques employed may be of independent interest.