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 , Eriksson, 1991 , Schroeder-Heister, 1993 , McDowell and Miller, 2000 ). Definitions are akin to logic programs, where the left and right rules...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.