English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  System Description: H-PILoT (Version 1.9)

Ihlemann, C., & Sofronie-Stokkermans, V.(2010). System Description: H-PILoT (Version 1.9) (ATR61). SFB/TR 14 AVACS.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-14C5-2 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-002C-482A-A
Genre: Report

Files

show Files
hide Files
:
avacs_technical_report_061.pdf (Abstract), 676KB
View   Save
File Permalink:
https://hdl.handle.net/11858/00-001M-0000-002C-454D-5
Name:
avacs_technical_report_061.pdf
Description:
-
OA-Status:
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
View
Copyright Date:
-
Copyright Info:
-
License:
-

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

Details

show
hide
Language(s): eng - English
 Dates: 2011-02-072010
 Publication Status: Issued
 Pages: 45 p.
 Publishing info: SFB/TR 14 AVACS
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 536340
Other: Local-ID: C125716C0050FB51-5F53450808E13ED9C125778C00501AE6-Ihlemann-Sofronie-Stokkermans-atr61-2010
Report Nr.: ATR61
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: AVACS Technical Report
  Abbreviation : ATR
  Other : SFB/TR 14 AVACS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 61 Sequence Number: - Start / End Page: - Identifier: ISSN: 1860-9821