17 citations · 31 across the 7 of their papers we have counts for
3 papers · 2 filters
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…