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.
.mli files) should be properly commented.If you have additional questions, please use
the github bugtracker or send me an
E-mail at simon dot cruanes at inria dot fr.
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
Home, Members, Software, Seminars