Observatorio de I+D+i UPM

Memorias de investigación
Research Publications in journals:
One-and-a-halfth-order Logic (journal version)
Year:2008
Research Areas
  • Programming language
Information
Abstract
The practice of first-order logic is replete with meta-level concepts. Most notably there are meta-variables ranging over formulae, variables, and terms, and properties of syntax such as alpha-equivalence, capture-avoiding substitution and assumptions about freshness of variables with respect to metavariables. We present one-and-a-halfth-order logic, in which these concepts are made explicit. We exhibit both sequent and algebraic specifications of one-and-a-halfth-order logic derivability, show them equivalent, show that the derivations satisfy cut-elimination, and prove correctness of an interpretation of first-order logic within it. We discuss the technicalities in a wider context as a case-study for nominal algebra, as a logic in its own right, as an algebraisation of logic, as an example of how other systems might be treated, and also as a theoretical foundation for future implementation.
International
Si
JCR
Si
Title
JOURNAL OF LOGIC AND COMPUTATION
ISBN
0955-792X
Impact factor JCR
0,821
Impact info
Volume
18
Journal number
4
From page
521
To page
562
Month
NOVIEMBRE
Ranking
Participants
  • Autor: Aad Mathijssen (Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands)
  • Autor: Murdoch Gabbay (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2020 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)