An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.
logtk.arith
sub-library, using either zarith or numTEF=1
)Release with the full power of higher-order and booleans as described in this paper.
This version contains major improvements from years of work on higher-order extensions to Superposition, including a new HO unification derived from JP unif. See papers on https://matryoshka-project.github.io/ :dancer:
upgrade on 1.5 with bugfixes, and more up-to-date dependencies (in particular, Iter and Msat).
(self-contained bundle with scripts to install opam and the dependencies is attached)
stable release