Sciweavers

Share
IANDC
2010

Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

10 years 7 months ago
Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
The Curry-Howard correspondence connects derivations in natural deduction with the lambdacalculus. Predicates are types, derivations are terms. This supports reasoning from assumptions to conclusions, but we may want to reason backwards; from the desired conclusion towards the assumptions. At intermediate stages we may have a partial derivation, with holes. This is natural in informal practice but it can be difficult to formalise. The informal act of filling holes in a partial derivation suggests a capturing substitution, since holes may occur in the
Murdoch James Gabbay, Dominic P. Mulligan
Added 03 Mar 2011
Updated 03 Mar 2011
Type Journal
Year 2010
Where IANDC
Authors Murdoch James Gabbay, Dominic P. Mulligan
Comments (0)
books