Cut elimination for a logic with induction and co-induction |
| |
Authors: | Alwen Tiu Alberto Momigliano |
| |
Institution: | 1. Research School of Computer Science, The Australian National University, Australia;2. Dipartimento di Scienze dell?Informazione, Università degli Studi di Milano, Italy |
| |
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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|