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.
We provide the following :