View on GitHub

zipperposition

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).

Zipperposition

Repository on github

Papers

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