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. In particular, it has the following features:

• Formulas and proofs for first-order and higher-order logic including equality reasoning, definitions, and inductive data types
• Sequent calculus, natural deduction, resolution refutations, expansion proofs
• Scriptable command-line interface
• Graphical user interface for viewing and transforming sequent calculus proofs, expansion proofs, etc.
• Basic proof transformations like regularization, Skolemization, interpolation, etc.
• Efficient translations between the implemented proof calculi
• Program extraction: modified realisability
• Gentzen-style cut-elimination
• Cut-Elimination by Resolution (ceres)
• Cut-Introduction
• Built-in superposition prover Escargot
• Built-in induction prover Viper
• Built-in intuitionistic prover Slakje
• Interfaces to automated reasoning tools:
  • resolution provers (all with proof import): Vampire, SPASS, E, Prover9, Metis
  • the connection-based theorem prover leanCoP (with proof import)
  • SMT-solvers for QF_UF: veriT (with proof import), Z3, CVC4
  • SAT-solvers: minisat, Glucose (with proof import), PicoSAT (with proof import), Sat4j (with proof import), and any DIMACS-compliant solver
  • MaxSAT-solvers: OpenWBO, Sat4j, toysolver

Releases

The latest release is version 2.17.0, from 2024-09-27: download. See the release notes for details on the latest changes. See the release archive for previous releases and source releases.

Documentation

• The user manual includes an accessible introduction to GAPT.
• For a more in-depth reference, consult the API documentation.

Development

GAPT is implemented in Scala. Development of GAPT is carried out on github, see our github repository. For more details, see also the developer wiki, the API documentation, or download the latest development build.

Publications

The best scientific reference to start reading about GAPT is:

• G. Ebner, S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, S. Zivota: System Description: GAPT 2.0, International Joint Conference on Automated Reasoning (IJCAR) 2016, N. Olivetti, A. Tiwari (eds.), Springer LNCS 9706.

The following is a list of publications related to the system. Some of them describe proof-theoretic algorithms which are implemented in GAPT, others describe a feature of the system or report on experiments carried out using GAPT.

• G. Ebner: Herbrand constructivization for automated intuitionistic theorem proving, TABLEAUX 2019. 355-373.
• G. Ebner: Fast cut-elimination using proof terms: an empirical study, CL&C 2018.
• G. Ebner, M. Schlaipfer: Efficient translation of sequent calculus proofs into natural deduction proofs, PAAR 2018.
• G. Ebner, S. Hetzl, A. Leitsch, G. Reis, D. Weller: On the generation of quantified lemmas, to appear in the Journal of Automated Reasoning, 2018.
• A. Leitsch, A. Lolic: Extraction of Expansion Trees, to appear in the Journal of Automated Reasoning, 2018.
• A. Leitsch, M. Lettmann: The problem of Π₂-cut-introduction, Theoretical Computer Science 706, 83-116, 2018.
• S. Eberhard, G. Ebner, S. Hetzl: Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars, ACM Transactions on Computational Logic 18(4), Art. 26, 2017.
• S. Hetzl, S. Eberhard: Inductive theorem proving based on tree grammars, Annals of Pure and Applied Logic 166(6), 665-700, 2015.
• G. Reis: Importing SMT and Connection proofs as expansion trees, PxTP 2015, 3-10.
• S. Hetzl, A. Leitsch, G. Reis and D. Weller: Algorithmic introduction of quantified cuts, Theoretical Computer Science, 549, 1-16, 2014.
• T. Libal, M. Riener, M. Rukhaia: Advanced Proof Viewing in ProofTool, UITP 2014, 35-47.
• S. Hetzl, A. Leitsch, G. Reis, J. Tapolczai and D. Weller: Introducing Quantified Cuts in Logic with Equality International Joint Conference on Automated Reasoning (IJCAR) 2014, S. Demri, D. Kapur and C. Weidenbach (eds.), Springer LNCS 8562.
• C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel Paleo: PROOFTOOL: a GUI for the GAPT Framework. UITP 2013, 1-14.
• S. Hetzl, T. Libal, M. Riener, and M. Rukhaia: Understanding Resolution Proofs through Herbrand's Theorem, Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013), D. Galmiche and D. Larchey-Wendling (eds.), Springer LNCS 8123.
• S. Hetzl: Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP), Conferences on Intelligent Computer Mathematics (CICM) 2012, J. Jeuring et al. (eds.), Springer LNAI 7362.
• S. Hetzl, A. Leitsch and D. Weller: Towards Algorithmic Cut-Introduction, Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), N. Bjørner, A. Voronkov (eds.), Springer LNCS 7180.
• S. Hetzl, A. Leitsch, D. Weller: CERES in Higher-Order Logic, Annals of Pure and Applied Logic 162(12), 1001-1034, 2011.
• M. Baaz, S. Hetzl, A. Leitsch, C. Richter and H. Spohr: CERES: An Analysis of Fürstenberg's Proof of the Infinity of Primes, Theoretical Computer Science 403(2-3), 160-175, 2008.
• M. Baaz, A. Leitsch: Cut-elimination and Redundancy-elimination by Resolution, Journal of Symbolic Computation 29(2), 149-177, 2000.

Support

• Vienna Science and Technology Fund (WWTF) via the Vienna Research Group VRG12-004: Structure and Expressivity
• Austrian Science Fund (FWF) project no. P25160: Algorithmic Structuring and Compression of Proofs
• Austrian Science Fund (FWF) project no. P24300: Proof Transformations via Cut-Elimination in Intuitionistic Logic
• joint French-Austrian ANR/FWF project no. I 383: About Schemata and Proofs
• Austrian Science Fund (FWF) project no. P22028: Proof-theoretic applications of CERES
• Georgian Shota Rustaveli National Science Foundation (SRNSF) project no. PG/6/4-102/13: Theorem Proving in Formula Schemata
• Georgian Shota Rustaveli National Science Foundation (SRNSF) project no. FR/51/4-102/13: Automated and Interactive Theorem Proving in Schemata and Unranked Logics.

---

Last Change: 2023-12-07