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.
Website: https://logic.at/gapt
Contact: mailing list
Example
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.
Installation
There are binary distributions available, you only need to have Java installed to run them:
wget https://logic.at/gapt/downloads/gapt-2.16.0.tar.gz
tar xf gapt-2.16.0.tar.gz
cd gapt-2.16.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.16.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.
System requirements
- Java 8 (or later)
- optional: external tools
- for development: sbt
License
GAPT is free software licensed under the GNU General Public License Version 3. See the file COPYING for details.