Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Ganzinger, Harald
Stuber, Jürgen

dblp
dblp

Not MPG Author(s):

Stuber, Jürgen

Editor(s):

Baader, Franz

dblp



BibTeX cite key*:

GanzingerStuber-2003-cade

Title, Booktitle

Title*:

Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation


_03CADE.1.ps (226.55 KB)

Booktitle*:

Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction

Event, URLs

URL of the conference:

http://www.cade-19.info/

URL for downloading the paper:

http://www.mpi-sb.mpg.de/~hg/pca.html#_03CADE.1

Event Address*:

Miami, Florida

Language:

English

Event Date*
(no longer used):

666

Organization:


Event Start Date:

28 July 2003

Event End Date:

2 August 2003

Publisher

Name*:

Springer

URL:

http://www.springer.com/

Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

2741

Number:


Month:

July

Pages:

335-349

Year*:

2003

VG Wort Pages:

15

ISBN/ISSN:

3-540-40559-3

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

The 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.



Download
Access Level:

Public

Correlation

MPG Unit:

MPI für Informatik



MPG Subunit:

AG 2

Audience:

Expert

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{GanzingerStuber-2003-cade,
AUTHOR = {Ganzinger, Harald and Stuber, J{\"u}rgen},
EDITOR = {Baader, Franz},
TITLE = {Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation},
BOOKTITLE = {Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction},
PUBLISHER = {Springer},
YEAR = {2003},
VOLUME = {2741},
PAGES = {335--349},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Miami, Florida},
MONTH = {July},
ISBN = {3-540-40559-3},
}


Entry last modified by Christine Kiesel, 01/28/2008
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Thomas Hillenbrand
Created
05/08/2003 11:48:47 AM
Revisions
24.
23.
22.
21.
20.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Edit Dates
17.06.2004 15:03:09
26.01.2004 11:50:14
26.01.2004 11:49:58
26.01.2004 11:39:41
07.07.2003 16:36:57
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
_03CADE.1.ps