Logtk is a free library for manipulating formal logic terms and formulas. It is licensed under the BSD2 license for the OCaml programming language.

Logtk provides several useful parts for logic-related implementations:

  • a library packed in a module Logtk, with terms, formulas, etc.;
  • small tools (see directory src/tools/) to illustrate how to use the library
    and provide basic services (type-checking, reduction to CNF, etc.);
  • an optional library in a module Logtk_meta,
    to provide reasoning at the problem level, about the presence of axiomatic theories. A small file describing a few theories can be found in data/builtin.theory and one of the tools, detect_theories, can be used straightforwardly.

Where to go next


If you have troubles of any kind, write to simon DOT cruanes AT inria DOT fr or to the bugtracker. Contributions, patches, and new features (e.g. parsers) are very welcome.