The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

DOI10.1017/S1471068420000423zbMath1477.03241arXiv2008.03714OpenAlexW3088695195MaRDI QIDQ5140030

Ekaterina Komendantskaya, Henning Basold, Dmitry Rozplokhas

Publication date: 13 December 2020

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2008.03714

zbMATH Keywords

cut eliminationsequent calculusHorn clausescoinductiontheory exploration

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items

On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ A coinductive approach to proof search through typed lambda-calculi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Lectures on the Curry-Howard isomorphism
• Fundamental properties of infinite trees
• Operational semantics of resolution and productivity in Horn clause logic
• Uniform proofs as a foundation for logic programming
• Proof Relevant Corecursive Resolution
• Programming with Higher-Order Logic
• Sequent calculi for induction and infinite descent
• Understanding functional dependencies via constraint handling rules
• Coinductive Logic Programming and Its Applications
• First-order Answer Set Programming as Constructive Proof Search
• Productive corecursion in logic programming
• Flexible coinductive logic programming
• Coinductive Logic Programming