H-PILoT

About H-PILoT

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.

The program was written by Carsten Ihlemann. It is implemented in OCaml.

Documentation

Manual
System Description (In Proc. CADE 22, LNAI 5663/2009, 131-139)
Extended System Description (AVACS Technical Report 61)

Sources

32-bit version: hpilot.32.opt
64-bit version: hpilot.opt