GAPT is a proof theory framework developed primarily at the Vienna University of Technology. GAPT contains data structures, algorithms, parsers and other components common in proof theory and automated deduction. In contrast to automated and interactive theorem provers whose focus is the construction of proofs, GAPT concentrates on the transformation and further processing of proofs.

Website: https://logic.at/gapt

Contact: mailing list

One of the many features GAPT supports is an implementation of Herbrand's theorem. Here is how you can automatically generate a Herbrand disjunction in GAPT:

Escargot.getExpansionProof(fof"P(c) ∨ P(d) → ∃x P(x)").map(_.deep)

which returns the following Herbrand disjunction (the quantifier on the right has been expanded):

Some( ⊢ P(c) ∨ P(d) → P(c) ∨ P(d))

You can also use Prover9, Vampire, EProver, and lots of other provers instead of the built-in Escargot prover, if you have them installed. There are many more examples in the user manual, and you can look into the API documentation for reference as well.

There are binary distributions available, you only need to have Java installed to run them:

wget https://logic.at/gapt/downloads/gapt-2.17.0.tar.gz
tar xf gapt-2.17.0.tar.gz
cd gapt-2.17.0
./gapt.sh

This will drop you into a scala REPL with GAPT pre-loaded.

If you want to use GAPT in your project, all you have to do is add the following line to your SBT build file:

libraryDependencies  = "at.logic.gapt" %% "gapt" % "2.17.0"

If you want to use the unstable git version of GAPT, you can use sbt console--this will drop you into the same environment as ./gapt.sh in the binary distribution.

See the wiki for more details.

• Java 8 (or later)
• optional: external tools like Vampire, SPASS, E and others. See the website for a complete list.
• for development: sbt

GAPT is free software licensed under the GNU General Public License Version 3. See the file COPYING for details.