Cut Elimination in Deduction Modulo by Abstract Completion

DOI10.1007/978-3-540-72734-7_9MaRDI QIDQ5434502zbMATH OpenOpenAlexFDO

Authors Guillaume Burel, Claude Kirchner

Publication date 4 January 2008

Published in Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00115556v3/file/bk_LFCS.pdf

zbMATH Keywords

abstract canonical systemautomated deduction and interactive theorem provingcut eliminationdeduction moduloKnuth-Bendix completionproof ordering

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Regaining cut admissibility in deduction modulo using abstract completion
• Cut Admissibility by Saturation
• On Constructive Cut Admissibility in Deduction Modulo
• Theorem proving modulo
• Orthogonality and Boolean Algebras for Deduction Modulo

Cited in

(9)

• Regaining cut admissibility in deduction modulo using abstract completion
• About folding-unfolding cuts and cuts modulo
• Algorithmic Equality in Heyting Arithmetic Modulo
• Canonicity!
• On Constructive Cut Admissibility in Deduction Modulo
• Axiom Directed Focusing
• Completeness for cut-based abduction
• Modular Cut-Elimination: Finding Proofs or Counterexamples
• Resolution is cut-free

This page was built for publication: Cut Elimination in Deduction Modulo by Abstract Completion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5434502)