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

• Type: Journal
• Year: 2010
• Where: IANDC
• Authors: Murdoch James Gabbay, Dominic P. Mulligan
• Keywords: Business, Curry-Howard Correspondence, IANDC 2010, Natural Deduction, Partial Derivation