Skip navigation
Skip navigation

Cut elimination for a logic with induction and co-induction

Tiu, Alwen; Momigliano, Alberto


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...[Show more]

CollectionsANU Research Publications
Date published: 2012
Type: Journal article
Source: Journal of Applied Logic
DOI: 10.1016/j.jal.2012.07.007


File Description SizeFormat Image
01_Tiu_Cut_elimination_for_a_logic_2012.pdf509.57 kBAdobe PDF    Request a copy
02_Tiu_Cut_elimination_for_a_logic_2012.pdf509.57 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator