17 citations · 31 across the 7 of their papers we have counts for
Showing 2014 · cs.LOShow all
3 papers · 2 filters
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.LO2014★ 1 cited
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…
cs.LO2014★ 1 cited
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…