Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles are based on a proof-theoretic (rather than set-theoretic) notion of definition (Hallnäs, 1991 [18], Eriksson, 1991 [11], Schroeder-Heister, 1993 [38], McDowell and Miller, 2000 [22]). Definitions are akin to logic programs, where the left and right rules for defined atoms allow one to view theories as “closed” or defining fixed points. The use of definitions and free equality makes it possible to reason intensionally about syntax. We add in a consistent way rules for pre- and post-fixed points, thus allowing the user to reason inductively and co-inductively about properties of computational system making full use of higher-order abstract syntax. Consistency is guaranteed via cut-elimination, where we give a direct cut-elimination procedure in the presence of general inductive and co-inductive definitions via the parametric reducibility technique.

Cut elimination for a logic with induction and co-induction / A. Tiu, A. Momigliano. - In: JOURNAL OF APPLIED LOGIC. - ISSN 1570-8683. - 10:4(2012), pp. 330-367. ((Intervento presentato al 6. convegno International Conference on Soft Computing Models in Industrial and Environmental Applications : April, 06 - 08 tenutosi a Salamanca (Spain) nel 2011 [10.1016/j.jal.2012.07.007].

Cut elimination for a logic with induction and co-induction

A. Momigliano
Ultimo
2012

Abstract

Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles are based on a proof-theoretic (rather than set-theoretic) notion of definition (Hallnäs, 1991 [18], Eriksson, 1991 [11], Schroeder-Heister, 1993 [38], McDowell and Miller, 2000 [22]). Definitions are akin to logic programs, where the left and right rules for defined atoms allow one to view theories as “closed” or defining fixed points. The use of definitions and free equality makes it possible to reason intensionally about syntax. We add in a consistent way rules for pre- and post-fixed points, thus allowing the user to reason inductively and co-inductively about properties of computational system making full use of higher-order abstract syntax. Consistency is guaranteed via cut-elimination, where we give a direct cut-elimination procedure in the presence of general inductive and co-inductive definitions via the parametric reducibility technique.
(Co-)induction; Cut-elimination; Higher-order abstract syntax; Logical frameworks; Parametric reducibility
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
Institute of Electrical and Electronic Engineers (IEEE)
Article (author)
File in questo prodotto:
File Dimensione Formato  
tiuapl.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 1.38 MB
Formato Adobe PDF
1.38 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/210544
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 21
  • ???jsp.display-item.citation.isi??? 8
social impact