View on GitHub


An automatic theorem prover in OCaml for typed higher-order logic with equality, datatypes and arithmetic, based on superposition+rewriting; supporting libraries for manipulating terms, formulas, clauses, etc. (including Logtk).


Repository on github


The slides of some of Simon Cruanes’ talks are on my page.

Some papers related to combinations of Superposition, higher-order logic, Induction, etc. can be found on Matryoshka’s website.

API Documentation

(obsolete) high-level documentation