Strict Basic Superposition

Bachmair, Leo; Ganzinger, Harald

Strict Basic Superposition

Bachmair, L., & Ganzinger, H. (1998). Strict Basic Superposition. In C., Kirchner, & H., Kirchner (Eds.), Proceedings of the 15th International Conference on Automated Deduction (CADE-98) (pp. 160-174). Berlin, Germany: Springer.

Item is 公開

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

基本情報

表示: 非表示:

アイテムのパーマリンク: https://hdl.handle.net/11858/00-001M-0000-000F-3891-1 版のパーマリンク: https://hdl.handle.net/11858/00-001M-0000-000F-3893-E

資料種別: 会議論文

ファイル

表示: ファイル

作成者

表示:

非表示:

作成者:
Bachmair, Leo¹, 著者
Ganzinger, Harald¹, 著者

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

内容説明

表示:

非表示:

キーワード: -

要旨: In this paper we solve a long-standing open problem by showing that strict superposition---that is, superposition without equality factoring---is refutationally complete. The difficulty of the problem arises from the fact that the strict calculus, in contrast to the standard calculus with equality factoring, is not compatible with arbitrary removal of tautologies, so that the usual techniques for proving the (refutational) completeness of paramodulation calculi are not directly applicable. We deal with the problem by introducing a suitable notion of {\em direct rewrite proof\/} and modifying proof techniques based on candidate models and counterexamples in that we define these concepts, not in terms of semantic truth, but in terms of direct provability. We introduce a corresponding concept of redundancy with which strict superposition is compatible and that covers most simplification techniques.

資料詳細

表示:

非表示:

言語: eng - English

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

出版の状態: 出版

ページ: -

出版情報: -

目次: -

査読: -

識別子（DOI, ISBNなど）: eDoc: 519696
その他: Local-ID: C1256104005ECAFC-FE42BE66528AE631C1256744004D8E7D-BachmairGanzinger-98-cade

学位: -

訴訟

表示:

Project information

表示:

出版物 1

表示:

非表示:

出版物名: Proceedings of the 15th International Conference on Automated Deduction (CADE-98)

種別: 会議論文集

著者・編者:
Kirchner, Claude, 編集者
Kirchner, Hélène, 編集者

所属:
-

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

ページ: - 巻号: - 通巻号: - 開始・終了ページ: 160 - 174 識別子（ISBN, ISSN, DOIなど）: ISBN: 3-540-64675-2

出版物 2

表示:

非表示:

出版物名: Lecture Notes in Artificial Intelligence

種別: 連載記事

著者・編者:

所属:

出版社, 出版地: -

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

アイテム詳細

基本情報

ファイル

関連URL

作成者

内容説明

資料詳細

関連イベント

訴訟

Project information

出版物 1

出版物 2