Abstract : 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 to represent
terms, formulas and substitutions, and algorithms to index terms, unify them.
It also contains parsers and a few tools to demonstrate its use. It is the basis
of a full-fledged superposition prover.
