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.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
- Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
- Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel: On the generation of quantified lemmas (2019)
- Färber, Michael; Kaliszyk, Cezary: Certification of nonclausal connection tableaux proofs (2019)
- Leitsch, Alexander; Lolic, Anela: Extraction of expansion trees (2019)
- Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
- Leitsch, Alexander; Lettmann, Michael: The problem of (\Pi_2)-cut-introduction (2018)
- Ebner, Gabriel; Hetzl, Stefan; Reis, Giselle; Riener, Martin; Wolfsteiner, Simon; Zivota, Sebastian: System description: GAPT 2.0 (2016)
- Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil: Understanding resolution proofs through Herbrand’s theorem (2013)