GAPT: General Architecture for Proof Theory
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.
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
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.10.tar.gz tar xf gapt-2.10.tar.gz cd gapt-2.10 ./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 two lines to your SBT build file:
resolvers += Resolver.jcenterRepo libraryDependencies += "at.logic.gapt" %% "gapt" % "2.10"
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.
GAPT is free software licensed under the GNU General Public License Version 3. See the file COPYING for details.