H-PILoT

 

Subproject

R1, H3

Categories

Core algorithms

Overview

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.

Publications

C. Ihlemann and V. Sofronie-Stokkermans. System description: H-PILoT. In Renate A. Schmidt, editor, Automated Deduction - CADE-22. 22nd International Conference on Automated Deduction, volume 5663 in Lecture Notes in Artifical Intelligence (LNAI), pages 131-139, 2009.

Benchmarks

H-PILoT benchmarks

Download

See www.mpi-inf.mpg.de/~ihlemann/software/index.html

Manual

Click here for the manual.

Status

Stable