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 , Eriksson, 1991 , Schroeder-Heister, 1993 , McDowell and Miller, 2000 ). 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.
|Titolo:||Cut elimination for a logic with induction and co-induction|
MOMIGLIANO, ALBERTO (Ultimo)
|Parole Chiave:||(Co-)induction; Cut-elimination; Higher-order abstract syntax; Logical frameworks; Parametric reducibility|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
Settore MAT/01 - Logica Matematica
|Data di pubblicazione:||2012|
|Enti collegati al convegno:||Institute of Electrical and Electronic Engineers (IEEE)|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1016/j.jal.2012.07.007|
|Appare nelle tipologie:||01 - Articolo su periodico|