MPI-INF Logo
Publications

Server    halma.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*:
13th Conference on Logic for Programming Artificial Intelligence Reasoning (LPAR'06)
Event, URLs
Conference URL::
http://www.lix.polytechnique.fr/~hermann/LPAR2006/
Downloading URL:
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.
Download
Access Level:
Public

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



BibTeX Entry:
@INPROCEEDINGS{GanKor:ThInst:2006,
AUTHOR = {Ganzinger, Harald and Korovin, Konstantin},
 EDITOR = {Hermann, Miki and Voronkov, Andrei},
 TITLE = {Theory Instantiation},
 BOOKTITLE = {13th Conference on Logic for Programming Artificial Intelligence Reasoning (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 Viorica Sofronie-Stokkermans, 12/05/2006
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
10/11/2006 04:45:15 PM
Revisions
2.
1.
0.

Editor(s)
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans

Edit Dates
12/05/2006 05:02:59 PM
10/11/2006 04:46:01 PM
10/11/2006 04:45:15 PM