-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
215 lines (188 loc) · 8.89 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<title>GAPT</title>
<link rel="stylesheet" href="style.css">
<link rel="stylesheet" href="ribbon.css">
</head>
<body>
<div class="box">
<div class="content">
<table>
<tr>
<td><img src="logo.png" alt="gapt logo"></td>
<td style="padding-left: 20px;"><h1>GAPT: General Architecture for Proof Theory</h1></td>
</table>
<div class="ribbon right grey">
<a href="https://github.com/gapt/gapt">Fork me on GitHub</a>
</div>
<p>
GAPT is a proof theory framework developed primarily at the <a href="http://www.tuwien.ac.at/">Vienna University of Technology</a>.
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:
</p>
<ul>
<li>Formulas and proofs for first-order and higher-order logic including equality reasoning, definitions, and inductive data types</li>
<li>Sequent calculus, natural deduction, resolution refutations, expansion proofs</li>
<li>Scriptable command-line interface</li>
<li>Graphical user interface for viewing and transforming sequent calculus proofs, expansion proofs, etc.</li>
<li>Basic proof transformations like regularization, Skolemization, interpolation, etc.</li>
<li>Efficient translations between the implemented proof calculi</li>
<li>Program extraction: modified realisability</li>
<li>Gentzen-style cut-elimination</li>
<li><a href="https://logic.at/ceres/">Cut-Elimination by Resolution (ceres)</a></li>
<li>Cut-Introduction</li>
<li>Built-in superposition prover Escargot</li>
<li>Built-in induction prover Viper</li>
<li>Built-in intuitionistic prover Slakje</li>
<li>Interfaces to automated reasoning tools:
<ul>
<li>resolution provers (all with proof import):
<a href="https://vprover.github.io/">Vampire</a>,
<a href="http://www.spass-prover.org/">SPASS</a>,
<a href="http://eprover.org/">E</a>,
<a href="http://www.cs.unm.edu/~mccune/prover9/">Prover9</a>,
<a href="http://www.gilith.com/software/metis/">Metis</a>
</li>
<li>the connection-based theorem prover <a href="http://www.leancop.de/">leanCoP</a> (with proof import)</li>
<li>SMT-solvers for QF_UF:
<a href="http://www.verit-solver.org/">veriT</a> (with proof import),
<a href="https://github.com/Z3Prover/z3">Z3</a>,
<a href="https://cvc4.github.io/">CVC4</a>
</li>
<li>SAT-solvers:
<a href="http://minisat.se/">minisat</a>,
<a href="http://www.labri.fr/perso/lsimon/glucose/">Glucose</a> (with proof import),
<a href="http://fmv.jku.at/picosat/">PicoSAT</a> (with proof import),
<a href="http://sat4j.org/">Sat4j</a> (with proof import),
and any DIMACS-compliant solver
</li>
<li>MaxSAT-solvers:
<a href="http://sat.inesc-id.pt/open-wbo/">OpenWBO</a>,
<a href="http://sat4j.org/">Sat4j</a>,
<a href="https://github.com/msakai/toysolver">toysolver</a>
</li>
</ul>
</li>
</ul>
<h2>Releases</h2>
<p>
The latest release is version 2.17.0, from 2024-09-27: <a href="downloads/gapt-2.17.0.tar.gz">download</a>.
See the <a href="https://github.com/gapt/gapt/blob/master/RELEASE-NOTES.md">release
notes</a> for details on the latest changes. See the <a href="release_archive.html">release archive</a>
for previous releases and source releases.
</p>
<h2>Documentation</h2>
<ul>
<li>The <a href="downloads/gapt-user-manual.pdf">user manual</a> includes an accessible introduction to GAPT.</li>
<li>For a more in-depth reference, consult the <a href="api/">API documentation</a>.</li>
</ul>
<h2>Development</h2>
<p>
GAPT is implemented in Scala. Development of GAPT is carried out
on github, see our <a href="https://github.com/gapt/gapt">github repository</a>. For more
details, see also the <a href="https://github.com/gapt/gapt/wiki">developer wiki</a>,
the <a href="api/">API documentation</a>, or download
the <a href="downloads/gapt-2.18.0-SNAPSHOT.tar.gz">latest development build</a>.
</p>
<h2>Publications</h2>
<p>
The best scientific reference to start reading about GAPT is:
</p>
<ul>
<li>
G. Ebner, S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, S. Zivota: <em>System Description: GAPT 2.0</em>, International
Joint Conference on Automated Reasoning (IJCAR) 2016, N. Olivetti, A. Tiwari (eds.), Springer LNCS 9706.
</li>
</ul>
<p>
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.
</p>
<ul>
<li>
G. Ebner: <em>Herbrand constructivization for automated intuitionistic theorem proving</em>, TABLEAUX 2019. 355-373.
</li>
<li>
G. Ebner: <em>Fast cut-elimination using proof terms: an empirical study</em>, CL&C 2018.
</li>
<li>
G. Ebner, M. Schlaipfer: <em>Efficient translation of sequent calculus proofs into natural deduction proofs</em>, PAAR 2018.
</li>
<li>
G. Ebner, S. Hetzl, A. Leitsch, G. Reis, D. Weller: <em>On the generation of quantified lemmas</em>, to appear in the Journal of Automated Reasoning, 2018.
</li>
<li>
A. Leitsch, A. Lolic: <em>Extraction of Expansion Trees</em>, to appear in the Journal of Automated Reasoning, 2018.
</li>
<li>
A. Leitsch, M. Lettmann: <em>The problem of Π<sub>2</sub>-cut-introduction</em>, Theoretical Computer Science 706, 83-116, 2018.
</li>
<li>
S. Eberhard, G. Ebner, S. Hetzl: <em>Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars</em>, ACM Transactions on Computational Logic 18(4), Art. 26, 2017.
</li>
<li>
S. Hetzl, S. Eberhard: <em>Inductive theorem proving based on tree grammars</em>, Annals of Pure and Applied Logic 166(6), 665-700, 2015.
</li>
<li>
G. Reis: <em>Importing SMT and Connection proofs as expansion trees</em>, PxTP 2015, 3-10.
</li>
<li>
S. Hetzl, A. Leitsch, G. Reis and D. Weller: <em>Algorithmic introduction of quantified cuts</em>,
Theoretical Computer Science, 549, 1-16, 2014.
</li>
<li>
T. Libal, M. Riener, M. Rukhaia: <em>Advanced Proof Viewing in ProofTool</em>, UITP 2014, 35-47.
</li>
<li>
S. Hetzl, A. Leitsch, G. Reis, J. Tapolczai and D. Weller: <em>Introducing Quantified Cuts in Logic with Equality</em>
International Joint Conference on Automated Reasoning (IJCAR) 2014, S. Demri, D. Kapur and C. Weidenbach (eds.), Springer LNCS 8562.
</li>
<li>
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.
</li>
<li>
S. Hetzl, T. Libal, M. Riener, and M. Rukhaia: <em>Understanding Resolution Proofs through Herbrand's Theorem</em>,
Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013), D. Galmiche and
D. Larchey-Wendling (eds.), Springer LNCS 8123.
</li>
<li>
S. Hetzl: <em>Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)</em>,
Conferences on Intelligent Computer Mathematics (CICM) 2012, J. Jeuring et al. (eds.), Springer LNAI 7362.
</li>
<li>
S. Hetzl, A. Leitsch and D. Weller: <em>Towards Algorithmic Cut-Introduction</em>,
Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), N. Bjørner, A. Voronkov (eds.), Springer LNCS 7180.
</li>
<li>
S. Hetzl, A. Leitsch, D. Weller: <em>CERES in Higher-Order Logic</em>, Annals of Pure and Applied Logic 162(12), 1001-1034, 2011.
</li>
<li>
M. Baaz, S. Hetzl, A. Leitsch, C. Richter and H. Spohr: <em>CERES: An Analysis of Fürstenberg's Proof of the Infinity of Primes</em>,
Theoretical Computer Science 403(2-3), 160-175, 2008.
</li>
<li>
M. Baaz, A. Leitsch: <em>Cut-elimination and Redundancy-elimination by Resolution</em>, Journal of Symbolic Computation 29(2),
149-177, 2000.
</li>
</ul>
<h2>Support</h2>
<ul>
<li>Vienna Science and Technology Fund (WWTF) via the <a href="https://wwtf.at/programmes/vienna_research_groups/VRG12-004">Vienna Research Group VRG12-004: Structure and Expressivity</a></li>
<li>Austrian Science Fund (FWF) project no. P25160: <a href="http://www.dmg.tuwien.ac.at/hetzl/ascop/">Algorithmic Structuring and Compression of Proofs</a></li>
<li>Austrian Science Fund (FWF) project no. P24300: Proof Transformations via Cut-Elimination in Intuitionistic Logic</li>
<li>joint French-Austrian ANR/FWF project no. I 383: <a href="https://logic.at/asap/">About Schemata and Proofs</a></li>
<li>Austrian Science Fund (FWF) project no. P22028: Proof-theoretic applications of CERES</li>
<li>Georgian Shota Rustaveli National Science Foundation (SRNSF) project no. PG/6/4-102/13: Theorem Proving in Formula Schemata</li>
<li>Georgian Shota Rustaveli National Science Foundation (SRNSF) project no. FR/51/4-102/13: Automated and Interactive Theorem Proving in Schemata and Unranked Logics.</li>
</ul>
<hr>
<p class="smallfont">Last Change: 2023-12-07</p>
</div>
</div>
</body>
</html>