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
Hillenbrand, Thomas
Waldmann, Uwe

dblp
dblp
dblp



Editor(s):

Baader, Franz

dblp

Not MPII Editor(s):

Baader, Franz

BibTeX cite key*:

GanzingerHillenbrandWaldmann2003

Title, Booktitle

Title*:

Superposition modulo a Shostak Theory


_03CADE.2.ps (211.47 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.2

Event Address*:

Miami, Florida

Language:

English

Event Date*
(no longer used):

July, 30 - August, 2

Organization:


Event Start Date:

30 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:

182-196

Year*:

2003

VG Wort Pages:

15

ISBN/ISSN:

3-540-40559-3

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

We investigate superposition modulo a Shostak theory $T$ in order to
facilitate reasoning in the amalgamation of $T$ and a free
theory~$F$.
%
Free operators occur naturally e.\,g.\ in program verification
problems when abstracting over subroutines. If their behaviour in
addition can be specified axiomatically, much more of the program
semantics can be captured.
%
Combining the Shostak-style components for deciding the clausal
validity problem with the ordering and saturation techniques
developed for equational reasoning, we derive a refutationally
complete calculus on mixed ground clauses which result for example
from CNF transforming arbitrary universally quantified formulae.
%
The calculus works modulo a Shostak theory in the sense that it
operates on canonizer normalforms. For the Shostak solvers that we
study, coherence comes for free: no coherence pairs need to be
considered.

Keywords:

Equational Reasoning, Saturation, Decision Procedures



Download
Access Level:

Public

Correlation

MPG Unit:

MPI für Informatik



MPG Subunit:

AG 2

Appearance:

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



BibTeX Entry:

@INPROCEEDINGS{GanzingerHillenbrandWaldmann2003,
AUTHOR = {Ganzinger, Harald and Hillenbrand, Thomas and Waldmann, Uwe},
EDITOR = {Baader, Franz},
TITLE = {Superposition modulo a {Shostak} Theory},
BOOKTITLE = {Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction},
PUBLISHER = {Springer},
YEAR = {2003},
VOLUME = {2741},
PAGES = {182--196},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Miami, Florida},
MONTH = {July},
ISBN = {3-540-40559-3},
}


Entry last modified by Christine Kiesel, 06/17/2004
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
04/04/2003 06:27:55 PM
Revisions
20.
19.
18.
17.
16.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Uwe Waldmann
Uwe Waldmann
Edit Dates
17.06.2004 14:59:19
17.06.2004 14:59:03
26.01.2004 11:47:06
01/09/2004 02:49:56 AM
08/02/2003 08:27:30 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
_03CADE.2.ps