Algorithmic Structuring and
Compression of Proofs

logo FWF
In this project we develop algorithms and software for structuring and compressing formal proofs. These algorithms are based on proof-theoretic results, in particular a recently discovered connection between proof theory and formal language theory. Please see the project description (or the poster) for more detailed information. This work is funded by the Austrian Science Fund (FWF) as project number P25160.


Our implementation is based on the GAPT project and is currently carried out in GAPT's codebase.


Last Change: 2016-04-13, Stefan Hetzl Valid HTML 4.01!