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
In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), pp.24-28 (Part II), Heidelberg, Germany, July, 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.
Supplementary materials are available :
Benchmarks: The benchmark OCaml programs (and also in SMT-LIB2 format for CVC4 and Z3) used in this page are available here. (mult-c.ml was fixed(2017/8/8))
VM: The virtural machine with the solver and it's README are VM and README_VM