Superposition with equivalence reasoning and delayed clause normal form 
transformation

Ganzinger, Harald; Stuber, Jürgen

Local TagsRelease HistoryDetailsSummary

Superposition with equivalence reasoning and delayed clause normal form transformation

Ganzinger, H., & Stuber, J. (2005). Superposition with equivalence reasoning and delayed clause normal form transformation. Information and Computation, 199, 3-23.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-27CA-E Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-27CB-C

Genre: Journal Article

Files

show Files

Locators

show

Creators

show

hide

Creators:
Ganzinger, Harald¹, Author
Stuber, Jürgen¹, Author

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

Content

show

hide

Free keywords: -

Abstract: This paper describes a superposition calculus where quantifiers are eliminated lazily. Superposition and simplification inferences may employ equivalences that have arbitrary formulas at their smaller side. A closely related calculus is implemented in the Saturate system and has shown useful on many examples, in particular in set theory. The paper presents a completeness proof and reports on practical experience obtained with the Saturate system.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2006-04-25Date issued: 2005

Publication Status: Issued

Pages: -

Publishing info: -

Table of Contents: -

Rev. Type: Peer

Identifiers: eDoc: 279087
Other: Local-ID: C1256104005ECAFC-0694A106EC9DC984C1257006003A5C14-Ganzinger-Stuber-ic-05

Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show

hide

Title: Information and Computation

Source Genre: Journal

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: 199 Sequence Number: - Start / End Page: 3 - 23 Identifier: -