View on GitHub

zipperposition

An automatic theorem prover in OCaml for typed 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 my (Simon Cruanes) talks are on my page

API Documentation

(obsolete) high-level documentation