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.

- Logtk : A Logic ToolKit for Automated Reasoning and its Implementation regarding the library of terms, formulas, and logic algorithms
- Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond (PhD thesis) contains explanations about the prover’s structure and its inductive and arithmetic abilities as of 2015.
- Superposition with Structural Induction is a more up to date description of the induction and rewriting sub-systems.
- Superposition for Lambda-Free Higher-Order Logic describes the newer improvements to the higher-order reasoning techniques.
- New Techniques for Higher-Order Superposition (draft)

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.