Logic toolkit, designed primarily for first-order automated reasoning. It aims at providing basic types and algorithms (terms, unification, orderings, indexing, etc.) that can be factored out of several applications, and also basic tools.

Logtk has a github page and is free software (see section License).


This project is licensed under the BSD2 license. See the LICENSE file.


If you have additional questions, please use the github bugtracker or send me an E-mail at simon dot cruanes at inria dot fr.


Via opam

The recommended way to install Logtk is through opam. Deducteam has its own opam repository whose adress is https://scm.gforge.inria.fr/anonscm/git/opam-deducteam/opam-deducteam.git . You need to have GMP (with headers) installed (it's not handled by opam). Once you installed GMP and opam, type:

$ opam repository add deducteam https://scm.gforge.inria.fr/anonscm/git/opam-deducteam/opam-deducteam.git

$ opam install logtk

This should install all OCaml dependencies. To upgrade the library, you'll need successively (to update package descriptions, then upgrade installed packages):

$ opam update

$ opam upgrade


If you really need to, you can download a release on the following github page for releases.

See the README file. In a nutshell, if all dependencies are installed:

$ ./configure

$ make install

Or, if you need, for instance, the meta-prover :

$ ./configure --enable-meta

$ make install

Parent page

Home, Members, Software, Seminars

logo inria logo deducteam