17 citations · 31 across the 7 of their papers we have counts for
7 papers
Expansion Trees with Cut
Federico Aschieri, Stefan Hetzl, Daniel Weller
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher…
Exposition: Synthesis via Functional Interpretation
Daniel Weller
The aim of this short paper is to give a practical introduction to functional interpretation of proofs for computer scientists interested in synthesis.
Introducing Quantified Cuts in Logic with Equality
Stefan Hetzl, Alexander Leitsch, Giselle Reis +2
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of…
Algorithmic Introduction of Quantified Cuts
Stefan Hetzl, Alexander Leitsch, Giselle Reis +1
We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computign a compressed representation of the terms pres…
Expansion Trees with Cut
Stefan Hetzl, Daniel Weller
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view it suggests a compact representation of proofs in classical first- and higher-…
PROOFTOOL: a GUI for the GAPT Framework
Cvetan Dunchev, Alexander Leitsch, Tomer Libal +4
This paper introduces PROOFTOOL, the graphical user interface for the General Architecture for Proof Theory (GAPT) framework. Its features are described with a focus not only on th…
CERES for First-Order Schemata
Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia +1
The cut-elimination method CERES (for first- and higher-order classical logic) is based on the notion of a characteristic clause set, which is extracted from an LK-proof and is alw…