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.
(obsolete) high-level documentation