Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




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

URL of the conference:

http://complogic.cs.mcgill.ca/cade22/

URL for downloading the paper:

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section