Cancellative superposition decides the theory of divisible torsion-free abelian 
groups

Waldmann, Uwe

アイテム詳細

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

一時保存へ追加

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

詳細要約

公開

報告書

Cancellative superposition decides the theory of divisible torsion-free abelian groups

MPS-Authors

/persons/resource/persons45689

Waldmann, Uwe
Automation of Logic, 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-1999-2-003.pdf
(全文テキスト（全般）), 304KB

付随資料 (公開)

There is no public supplementary material available

引用

Waldmann, U.(1999). Cancellative superposition decides the theory of divisible torsion-free abelian groups (MPI-I-1999-2-003). Saarbrücken: Max-Planck-Institut für Informatik.

引用: https://hdl.handle.net/11858/00-001M-0000-0014-6F75-5

要旨

In divisible torsion-free abelian groups, the efficiency of the cancellative superposition calculus can be greatly increased by combining it with a variable elimination algorithm that transforms every clause into an equivalent clause without unshielded variables. We show that the resulting calculus is a decision procedure for the theory of divisible torsion-free abelian groups.