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.