Strict Basic Superposition

Bachmair, Leo; Ganzinger, Harald

Local TagsRelease HistoryDetailsSummary

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 Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3891-1 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3893-E

Genre: Conference Paper

Files

show Files

Locators

show

Creators

show

hide

Creators:
Bachmair, Leo¹, Author
Ganzinger, Harald¹, Author

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

Content

show

hide

Free keywords: -

Abstract: 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.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2010-03-12Date issued: 1998

Publication Status: Issued

Pages: -

Publishing info: -

Table of Contents: -

Rev. Type: -

Identifiers: eDoc: 519696
Other: Local-ID: C1256104005ECAFC-FE42BE66528AE631C1256744004D8E7D-BachmairGanzinger-98-cade

Degree: -

Event

show

hide

Title: Untitled Event

Place of Event: Lindau, Germany

Start-/End Date: 1998

Legal Case

show

Project information

show

Source 1

show

hide

Title: Proceedings of the 15th International Conference on Automated Deduction (CADE-98)

Source Genre: Proceedings

Creator(s):
Kirchner, Claude, Editor
Kirchner, Hélène, Editor

Affiliations:
-

Publ. Info: Berlin, Germany : Springer

Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 160 - 174 Identifier: ISBN: 3-540-64675-2

Source 2

show

hide

Title: Lecture Notes in Artificial Intelligence

Source Genre: Series

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: 1421 Sequence Number: - Start / End Page: - Identifier: -