## 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.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.

### 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.