Cut elimination for a logic with induction and co-induction
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Journal of Applied Logic|
|01_Tiu_Cut_elimination_for_a_logic_2012.pdf||509.57 kB||Adobe PDF||Request a copy|
|02_Tiu_Cut_elimination_for_a_logic_2012.pdf||509.57 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.