Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Simon Cruanes · EPiC series in computing · 2018
We describe the design and implementation of Logtk, an OCaml library for writing automated reasoning tools that deal with (possibly typed) first-order logic. The library provides data structures and algorithms to represent terms, formulas, substitutions, perform unification, index terms, parse problems, as well as a few tools to demonstrate itsuse. It is the basis of a full-fledged superposition prover.