Technical, Research Report
@TechReport
Technischer-, Forschungsbericht


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):

Bernd, Becker
Damm, Werner
Fränzle, Martin
Olderog, Ernst-Rüdiger
Podelski, Andreas
Wilhelm, Reinhard

dblp
dblp
dblp
dblp
dblp
dblp

Not MPII Editor(s):

Bernd, Becker
Damm, Werner
Fränzle, Martin
Olderog, Ernst-Rüdiger
Podelski, Andreas
Wilhelm, Reinhard

BibTeX Citekey*:

Ihlemann-Sofronie-Stokkermans-atr61-2010

Language:

English

Title, Institution

Title*:

System Description: H-PILoT (Version 1.9)

Institution*:

Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)

Publishers or Institutions Address*:

Saarbrücken

Type:

Technical Report

No, Year, pp.,

Number*:

ATR 61

Pages*:

45

Month:

August

VG Wort
Pages*:


Year*:

2010

ISBN/ISSN:

1860-9821





DOI:




Note, Abstract, ©

Note:


(LaTeX) Abstract:

This system description provides an overview of H-PILoT
(Hierarchical Proving by Instantiation in Local Theory
extensions), a program for hierarchical reasoning in
extensions of logical theories.
H-PILoT reduces deduction problems in the theory extension
to deduction problems in the base theory.
Specialized provers and standard SMT solvers can be used
for testing the satisfiability of the formulae obtained
after the reduction. For a certain type of theory extension
(namely for {\em local theory extensions}) this
hierarchical reduction is sound and complete and --
if the formulae obtained this way belong to a fragment
decidable in the base theory -- H-PILoT provides a decision
procedure for testing satisfiability of ground formulae,
and can also be used for model generation.

Categories / Keywords:


Copyright Message:


HyperLinks / References / URLs:


Personal Comments:


File Upload:


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:
@TECHREPORT{Ihlemann-Sofronie-Stokkermans-atr61-2010,
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Bernd, Becker and Damm, Werner and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {System Description: {H-PILoT} (Version 1.9)},
YEAR = {2010},
TYPE = {Technical Report},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
NUMBER = {ATR 61},
PAGES = {45},
ADDRESS = {Saarbr{\"u}cken},
MONTH = {August},
ISBN = {1860-9821},
}


Entry last modified by Anja Becker, 02/07/2011
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
08/27/2010 04:34:57 PM
Revisions
3.
2.
1.
0.
Editor(s)
Anja Becker
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
07.02.2011 11:23:24
09/10/2010 02:20:59 PM
08/27/2010 04:36:02 PM
08/27/2010 04:34:57 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section