On Using Ground Joinable Equations in Equational Theorem Proving

Avenhaus, Jürgen; Hillenbrand, Thomas; Löchner, Bernd

アイテム詳細

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

一時保存へ追加

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

公開

学術論文

On Using Ground Joinable Equations in Equational Theorem Proving

MPS-Authors

/persons/resource/persons44621

Hillenbrand, Thomas
International Max Planck Research School, MPI for Informatics, Max Planck Society;
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44934

Löchner, Bernd
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

引用

Avenhaus, J., Hillenbrand, T., & Löchner, B. (2003). On Using Ground Joinable Equations in Equational Theorem Proving. Journal of Symbolic Computation, 36, 217-233.

引用: https://hdl.handle.net/11858/00-001M-0000-000F-2DA8-E

要旨

When rewriting and completion techniques are used for equational theorem proving, the axiom set is saturated with the aim to get a rewrite system that is terminating and confluent on ground terms. To reduce the computational effort it should (1) be powerful for rewriting and (2) create not too many critical pairs. These problems become especially important if some operators are associative and commutative (\AC). We show in this paper how these two goals can be reached to some extent by using ground joinable equations for simplification purposes and omitting them from the generation of new facts. % For the special case of \AC-operators we present a simple redundancy criterion which is easy to implement, efficient, and effective in practice, leading to significant speed-ups.