Cut-elimination for a logic with definitions and induction

DOI10.1016/S0304-3975(99)00171-1zbMath0951.03050MaRDI QIDQ1575931

Raymond McDowell, Dale A. Miller

Publication date: 23 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

sequent calculusinductionintuitionistic logiccut-eliminationlogic specification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Cut-elimination and normal-form theorems (03F05)

Related Items

The undecidability of proof search when equality is a logical connective, Proof checking and logic programming, Cut-Elimination and Proof Schemata, A two-level logic approach to reasoning about computations, Schematic refutations of formula schemata, Nominal abstraction, A Survey of the Proof-Theoretic Foundations of Logic Programming, Encoding transition systems in sequent calculus, Cut elimination for a logic with induction and co-induction, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, A rewriting framework and logic for activities subject to regulations, Unnamed Item, A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains, Focused Inductive Theorem Proving, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, On the Role of Names in Reasoning about λ-tree Syntax Specifications, Least and Greatest Fixed Points in Linear Logic, Schematic Cut Elimination and the Ordered Pigeonhole Principle, Non-well-founded deduction for induction and coinduction, Lexicographic Path Induction, Axiom Directed Focusing, Mechanized metatheory revisited, Encoding Generic Judgments, A proof theory for model checking, Integrating induction and coinduction via closure operators and proof cycles

Cites Work

• Forum: A multiple-conclusion specification logic
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Uniform proofs as a foundation for logic programming
• Higher-order Horn clauses
• Logic Programming with Focusing Proofs in Linear Logic
• CUT-PROPERTY AND NEGATION AS FAILURE
• Intensional interpretations of functionals of finite type I
• The practice of logical frameworks
• Solution to a problem of Ono and Komori
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item