Observatorio de I+D+i UPM

Memorias de investigación
Artículos en revistas:
Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
Áreas de investigación
  • Ciencias de la computación y tecnología informática
The Curry-Howard correspondence connects derivations in natural deduction with the lambda-calculus. 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 scope of quantifier introduction rules. As other authors have observed, this is not immediately supported by the lambda-calculus. Also, universal quantification requires a `fresh name¿ and it is not immediately obvious what formal meaning to assign to this notion if derivations are incomplete. Further issues arise with proof-normalisation; this corresponds with lambda-calculus reduction, which can require alpha-conversion to avoid capture when beta-reducing, and it is not immediately clear how to alpha-convert a name in an incomplete derivation. We apply a one-and-a-half level technique based on nominal terms to construct a Curry- Howard correspondence for first-order logic. This features two levels of variable, but with no lambda-abstraction at the second level. Predicates are types, derivations are terms, proof-normalisation is reduction ¿ and the two levels of variable are, respectively, the assumptions and the holes of an incomplete derivation. We give notions of proof-term, typing, alpha-conversion and beta-reduction for our syntax. We prove confluence, we exhibit several admissible rules including a proof that instantiation of level two variables is type-safe ¿ this corresponds with the act of filling holes in an incomplete derivation, and can be viewed as a form of Cut-rule ¿ and we explore the connection with traditional Curry-Howard in the case that the derivation is in fact complete. Our techniques are not specifically tailored to first-order logic and the same ideas should be applicable without any essential new difficulties to similar logical systems.
Título de la revista
Factor de impacto JCR
Información de impacto
Número de revista
Desde la página
Hasta la página
Esta actividad pertenece a memorias de investigación
  • Autor: Murdoch Gabbay (UPM)
  • Participante: Dominic P. Mulligan (Heriot-Watt University, Scotland, UK)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
S2i 2023 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)