8 citations · 8 across the 2 of their papers we have counts for
2 papers
cs.LO2014
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.
cs.LO2013★ 8 cited
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…