MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Ganzinger, Harald
Korovin, Konstantin		dblp
dblp
Not MPG Author(s):
Korovin, Konstantin
Editor(s):
Hermann, Miki
Voronkov, Andrei		dblp
dblp
Not MPII Editor(s):
Hermann, Miki
Voronkov, Andrei
BibTeX cite key*:
GanKor:ThInst:2006
Title, Booktitle
Title*:
Theory Instantiation
Booktitle*:
Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06)
Event, URLs
Conference URL::
http://www.lix.polytechnique.fr/~hermann/LPAR2006/
Downloading URL:
http://www.springerlink.com/content/3k2m244417877355/fulltext.pdf
Event Address*:
Phnom Penh, Cambodia
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
13 November 2006
Event End Date:
17 November 2006
Publisher
Name*:
Springer
URL:
http://www.springer-ny.com/
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
4246
Number:
Month:
Pages:
497-511
Year*:
2006
VG Wort Pages:
ISBN/ISSN:
3-540-4828-4
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
In this paper we present a method of integrating theory
reasoning into the instantiation framework. One of the distinctive features of our approach is that it allows
us to employ off-the-shelf satisfiability solvers for ground
clauses modulo theories, as a part of general first-order
reasoning. As an application of this approach, we show how
it is possible to combine the instantiation calculus with
other calculi, such as ordered resolution and paramodulation.
URL for the Abstract:
http://dx.doi.org/10.1007/11916277_34
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort



BibTeX Entry:

@INPROCEEDINGS{GanKor:ThInst:2006,
AUTHOR = {Ganzinger, Harald and Korovin, Konstantin},
 EDITOR = {Hermann, Miki and Voronkov, Andrei},
 TITLE = {Theory Instantiation},
 BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06)},
 PUBLISHER = {Springer},
 YEAR = {2006},
 VOLUME = {4246},
 PAGES = {497--511},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Phnom Penh, Cambodia},
 ISBN = {3-540-4828-4},
}

Entry last modified by Christine Kiesel, 03/12/2007
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)
Viorica Sofronie-Stokkermans		Created
03/12/2007 10:44:25 AM
Revisions
3.
2.
1.
0.
Editor(s)
Christine Kiesel
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
15.02.2007 09:32:42
12/05/2006 05:02:59 PM
10/11/2006 04:46:01 PM
10/11/2006 04:45:15 PM