Induction and Co-induction in Sequent Calculus

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 actually based on a proof theoretic notion of definition, following on work by Schroeder-Heister, Girard, and McDowell and Miller. Definitions are essentially stratified logic programs. The left and right rules for defined atoms treat the definitions as defining fixed points. The use of definitions also makes it possible to reason intensionally about syntax, in particular enforcing free equality via unification. The full system thus allows inductive and co-inductive proofs g higher-order abstract syntax. We extended the earlier work by allowing induction and co-induction on general definitions and show that cut-elimination holds for this extension. We present some examples involving lazy lists and simulation in lazy -calculus. Two prot...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Alwen Tiu, Alberto Momigliano
• Keywords: CORR 2008, Education, Proof Principles, Proof Search, Proof Theoretic Notion