Combining Algebra and Universal Algebra in First-Order Theorem Proving: The 
Case of Commutative Rings

Bachmair, Leo; Ganzinger, Harald; Stuber, Jürgen

doi:10.1007/BFb0014420

Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings

Bachmair, L., Ganzinger, H., & Stuber, J. (1995). Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings. In E., Astesiano, G., Reggio, & A., Tarlecki (Eds.), Recent Trends in Data Type Specification (pp. 1-29). Berlin, Germany: Springer.

Item is 公開

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

基本情報

表示: 非表示:

アイテムのパーマリンク: https://hdl.handle.net/11858/00-001M-0000-0014-ACF0-7 版のパーマリンク: https://hdl.handle.net/21.11116/0000-000E-57B6-3

資料種別: 会議論文

ファイル

表示: ファイル

作成者

表示:

非表示:

作成者:
Bachmair, Leo¹, 著者
Ganzinger, Harald¹, 著者
Stuber, Jürgen¹, 著者

所属:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

内容説明

表示:

非表示:

キーワード: -

要旨: We present a general approach for integrating certain mathematical structures
in first-order equational theorem provers. More specifically, we consider
theorem proving problems specified by sets of first-order clauses that contain
the axioms of a commutative ring with a unit element. Associative-commutative
superposition forms the deductive core of our method, while a convergent
rewrite system for commutative rings provides a starting point for more
specialized inferences tailored to the given class of formulas. We adopt ideas
from the Gr{\"o}bner basis method to show that many inferences of the
superposition calculus are redundant. This result is obtained by the judicious
application of the simplification techniques afforded by convergent rewriting
and by a process called symmetrization that embeds inferences between single
clauses and ring axioms.

資料詳細

表示:

非表示:

言語: eng - English

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

出版の状態: 出版

ページ: -

出版情報: -

目次: -

査読: -

識別子（DOI, ISBNなど）: eDoc: 519585
その他: Local-ID: C1256104005ECAFC-AA56DA80C58704F6C125614C004A6F13-BachmairGanzingerStuber-95-compass
DOI: 10.1007/BFb0014420
BibTex参照ID: Bachmair-et-al_ COMPASS-ADT95

学位: -

訴訟

表示:

Project information

表示:

出版物 1

表示:

非表示:

出版物名: Recent Trends in Data Type Specification

副タイトル : 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30 - June 3, 1994. Selected Papers

省略形 : COMPASS/ADT 1995

種別: 会議論文集

著者・編者:
Astesiano, Egidio¹, 編集者
Reggio, Gianna¹, 編集者
Tarlecki, Andrzej¹, 編集者

所属:
1 External Organizations, ou_persistent22

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

ページ: - 巻号: - 通巻号: - 開始・終了ページ: 1 - 29 識別子（ISBN, ISSN, DOIなど）: ISBN: 978-3-540-59132-0

出版物 2

表示:

非表示:

出版物名: Lecture Notes in Computer Science

省略形 : LNCS

種別: 連載記事

著者・編者:

所属:

出版社, 出版地: -

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

アイテム詳細

基本情報

ファイル

関連URL

作成者

内容説明

資料詳細

関連イベント

訴訟

Project information

出版物 1

出版物 2