English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  System Description: H-PILoT

Ihlemann, C., & Sofronie-Stokkermans, V. (2009). System Description: H-PILoT. In R. Schmidt (Ed.), Automated Deduction - CADE-22 (pp. 131-139). Berlin: Springer. doi:10.1007/978-3-642-02959-2_9.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1A75-4 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BB7F-B
Genre: Conference Paper
Latex : System Description: {H-PILoT}

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Ihlemann, Carsten1, Author           
Sofronie-Stokkermans, Viorica1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2010-02-0420092009
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 521092
Other: Local-ID: C125716C0050FB51-4D901D8754AEDFA9C12575A0003BDE0D-hpilot2009
DOI: 10.1007/978-3-642-02959-2_9
 Degree: -

Event

show
hide
Title: 22nd International Conference on Automated Deduction
Place of Event: Montreal, Canada
Start-/End Date: 2009-08-02 - 2009-08-07

Legal Case

show

Project information

show

Source 1

show
hide
Title: Automated Deduction - CADE-22
  Subtitle : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings
  Abbreviation : CADE 2009
Source Genre: Proceedings
 Creator(s):
Schmidt, Renate1, Editor
Affiliations:
1 External Organizations, ou_persistent22            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 131 - 139 Identifier: ISBN: 978-3-642-02958-5

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
  Abbreviation : LNAI
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 5663 Sequence Number: - Start / End Page: - Identifier: ISSN: 0302-9743