GitHub repository: sneeuwballen/zipperposition
Primary language: OCaml
Description: An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.