Computer Science – Logic in Computer Science
Scientific paper
2010-09-03
Computer Science
Logic in Computer Science
43 pages; A version of this system description appeared as AVACS technical report Nr. 61 (SFB/TR 14) http://www.avacs.org
Scientific paper
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 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.
Ihlemann Carsten
Sofronie-Stokkermans Viorica
No associations
LandOfFree
System Description: H-PILoT (Version 1.9) does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with System Description: H-PILoT (Version 1.9), we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System Description: H-PILoT (Version 1.9) will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-684965