MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
dblp
dblp
Editor(s):
Schmidt, Renate A.dblp
BibTeX cite key*:
hpilot2009
Title, Booktitle
Title*:
System Description: H-PILoT
Booktitle*:
Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction
Event, URLs
Conference URL::
http://complogic.cs.mcgill.ca/cade22/
Downloading URL:
http://dx.doi.org/10.1007/978-3-642-02959-2_9
Event Address*:
Montreal, Canada
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
2 August 2009
Event End Date:
7 August 2009
Publisher
Name*:
Springer
URL:
http://www.springer-ny.com/
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Artificial Intelligence
Volume:
5663
Number:
Month:
August
Pages:
131-139
Year*:
2009
VG Wort Pages:
ISBN/ISSN:
978-3-642-02958-5
Sequence Number:
DOI:
10.1007/978-3-642-02959-2_9
Note, Abstract, ©
(LaTeX) Abstract:
H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions)
is a program for hierarchical reasoning in extensions of logical theories with
additional functions axiomatized by a set of (universally quantified) clauses:
deduction problems in the theory extension are reduced to deduction problems
in the base theory. Specialized provers, as well as standard SMT solvers, are
then used for testing the satisfiability of the formulae obtained after the
reduction. The hierarchical reduction used in H-PILoT is always sound; it
is complete for the class of so-called local extensions of a base theory.

If the clauses obtained by this reduction belong to a fragment decidable in
the base theory, H-PILoT provides a decision procedure for testing
satisfiability of ground formulae w.r.t.\ a theory extension, and can also
be used for model generation. This is the major advantage of H-PILoT compared
with other state-of-the art SMT solvers. H-PILoT can alternatively be used as
a tool for ``steering'' the instantiation mechanism of standard SMT provers,
in order to provide decision procedures in the case of local theory extensions.

This system description provides an overview of H-PILoT and illustrates on
some examples the main advantage of using H-PILoT for satisfiability
checking in local extensions, in comparison with the performance of general
state of the art SMT-provers.
Keywords:
Local Reasoning, Verification, Satisfiability Modulo Theory
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{hpilot2009,
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Schmidt, Renate A.},
TITLE = {System Description: {H-PILoT}},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PUBLISHER = {Springer},
YEAR = {2009},
VOLUME = {5663},
PAGES = {131--139},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Montreal, Canada},
MONTH = {August},
ISBN = {978-3-642-02958-5},
ISBN = {0302-9743},
DOI = {10.1007/978-3-642-02959-2_9},
}


Entry last modified by Anja Becker, 03/25/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)
[Library]
Created
04/22/2009 12:53:54 PM
Revisions
3.
2.
1.
0.
Editor(s)
Anja Becker
Carsten Ihlemann
Carsten Ihlemann
Carsten Ihlemann
Edit Dates
25.03.2010 11:51:55
02/04/2010 04:53:27 PM
05/29/2009 04:16:11 PM
04/22/2009 12:53:54 PM