MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe		dblp
dblp
dblp
Editor(s):
Baader, Franzdblp
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
Conference URL::
http://www.cade-19.info/
Downloading URL:
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
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

File Attachment Icon
_03CADE.2.ps