MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Ganzinger, Haralddblp
Editor(s):
Voronkov, Andreidblp
Not MPII Editor(s):
Voronkov, Andrei
BibTeX cite key*:
Ganzinger-02-cade
Title, Booktitle
Title*:
Shostak Light
_02CADE.pdf (175.53 KB)
Booktitle*:
Automated deduction, CADE-18 : 18th International Conference on Automated Deduction
Event, URLs
Conference URL::
http://www.uni-koblenz.de/~cade-18/
Downloading URL:
http://www.mpi-sb.mpg.de/~hg/papers/conferences/_02CADE.pdf
Event Address*:
Copenhagen, Denmark
Language:
English
Event Date*
(no longer used):
-- July, 27-30, 2002
Organization:
Event Start Date:
27 July 2002
Event End Date:
30 July 2002
Publisher
Name*:
Springer
URL:
http://www.springer.com/
Address*:
Heidelberg, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Artificial Intelligence
Volume:
2392
Number:
Month:
Pages:
332-346
Year*:
2002
VG Wort Pages:
15
ISBN/ISSN:
3-540-43931-5
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We represent the essential ingredients of Shostak's procedure at a high level of abstraction, and as a refinement of the Nelson-Oppen procedure. We analyze completeness issues of the method based on a general notion of theories. We also formalize a notion of sigma-models and show that on the basis of Shostak's procedure we cannot distinguish a theory from its approximation represented by the class of its sigma-models.
Keywords:
Theorem Proving
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
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{Ganzinger-02-cade,
AUTHOR = {Ganzinger, Harald},
 EDITOR = {Voronkov, Andrei},
 TITLE = {Shostak Light},
 BOOKTITLE = {Automated deduction, CADE-18 : 18th International Conference on Automated Deduction},
 PUBLISHER = {Springer},
 YEAR = {2002},
 VOLUME = {2392},
 PAGES = {332--346},
 SERIES = {Lecture Notes in Artificial Intelligence},
 ADDRESS = {Copenhagen, Denmark},
 ISBN = {3-540-43931-5},
}

Entry last modified by Christine Kiesel, 03/12/2010
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/16/2002 02:42:20 PM
Revisions
18.
17.
16.
15.
14.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
17.06.2004 14:45:53
01.09.2003 17:23:46
01.09.2003 14:20:28
01.09.2003 14:19:47
01.08.2003 15:47:42

File Attachment Icon
_02CADE.pdf