This page demonstrates the induction-based Horn constraint solver proposed in the following paper:
Automating Induction for Solving Horn Clauses
Hiroshi Unno, Sho Torii, and Hiroki Sakamoto
To appear in CAV 2017.
The Horn constraint solver is here used as a backend of RCaml, which is an extension of the OCaml functional language with refinement type checking and inference features based on Horn constraint solving. The benchmark OCaml programs used in this page are available here.