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

View the Project on GitHub sneeuwballen/zipperposition


Repository on github


The slides of some of Simon Cruanes’ talks are on his 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