Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  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

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1A75-4 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BB7F-B
Genre: Konferenzbeitrag
Latex : System Description: {H-PILoT}

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Ihlemann, Carsten1, Autor           
Sofronie-Stokkermans, Viorica1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-02-0420092009
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 521092
Anderer: Local-ID: C125716C0050FB51-4D901D8754AEDFA9C12575A0003BDE0D-hpilot2009
DOI: 10.1007/978-3-642-02959-2_9
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: 22nd International Conference on Automated Deduction
Veranstaltungsort: Montreal, Canada
Start-/Enddatum: 2009-08-02 - 2009-08-07

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Automated Deduction - CADE-22
  Untertitel : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings
  Kurztitel : CADE 2009
Genre der Quelle: Konferenzband
 Urheber:
Schmidt, Renate1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 131 - 139 Identifikator: ISBN: 978-3-642-02958-5

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Artificial Intelligence
  Kurztitel : LNAI
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 5663 Artikelnummer: - Start- / Endseite: - Identifikator: ISSN: 0302-9743