Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)

Ganzinger, Harald; Waldmann, Uwe

doi:10.1007/3-540-61511-3_102

Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)

Ganzinger, H., & Waldmann, U. (1996). Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). In M. A., McRobbie, & J. K., Slaney (Eds.), Automated Deduction - CADE-13 (pp. 388-402). Berlin, Germany: Springer.

Item is 公開

表示: 全項目非表示: 全項目

基本情報

表示: 非表示:

アイテムのパーマリンク: https://hdl.handle.net/11858/00-001M-0000-0014-AC21-A 版のパーマリンク: https://hdl.handle.net/21.11116/0000-000E-38D8-0

資料種別: 会議論文

ファイル

表示: ファイル

作成者

表示:

非表示:

作成者:
Ganzinger, Harald¹, 著者
Waldmann, Uwe^{1, 2}, 著者

所属:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545

内容説明

表示:

非表示:

キーワード: -

要旨: Cancellative abelian monoids encompass abelian groups,
but also such ubiquitous structures as the natural numbers or
multisets. Both the AC axioms and the cancellation law are
difficult for a general purpose theorem prover, as they create
many variants of clauses which contain sums. We describe a
refined superposition calculus for cancellative abelian monoids
which requires neither explicit inferences with the theory clauses
nor extended equations or clauses. Strong ordering constraints
allow us to restrict to inferences that involve the maximal term
of the maximal sum in the maximal literal. Besides, the search
space is reduced drastically by variable elimination techniques.

資料詳細

表示:

非表示:

言語: eng - English

日付: 修正: 2010-03-12出版: 1996

出版の状態: 出版

ページ: -

出版情報: -

目次: -

査読: -

識別子（DOI, ISBNなど）: eDoc: 519898
その他: Local-ID: C1256104005ECAFC-D3B31BC55873B750C12564610057884F-GanzingerWaldmann1996CADE
BibTex参照ID: Ganzinger-Waldmann_CADE96
DOI: 10.1007/3-540-61511-3_102

学位: -

訴訟

表示:

Project information

表示:

出版物 1

表示:

非表示:

出版物名: Automated Deduction - CADE-13

副タイトル : 13th International Conference on Automated Deduction

省略形 : CADE 1996

種別: 会議論文集

著者・編者:
McRobbie, Michael A.¹, 編集者
Slaney, John K.¹, 編集者

所属:
1 External Organizations, ou_persistent22

出版社, 出版地: Berlin, Germany : Springer

ページ: - 巻号: - 通巻号: - 開始・終了ページ: 388 - 402 識別子（ISBN, ISSN, DOIなど）: ISBN: 978-3-540-61511-8

出版物 2

表示:

非表示:

出版物名: Lecture Notes in Artificial Intelligence

省略形 : LNAI

種別: 連載記事

著者・編者:

所属:

出版社, 出版地: -

ページ: - 巻号: 1104 通巻号: - 開始・終了ページ: - 識別子（ISBN, ISSN, DOIなど）: -

アイテム詳細

基本情報

ファイル

関連URL

作成者

内容説明

資料詳細

関連イベント

訴訟

Project information

出版物 1

出版物 2