Cut Elimination in Deduction Modulo by Abstract Completion

DOI10.1007/978-3-540-72734-7_9zbMath1132.03315OpenAlexW1526059592MaRDI QIDQ5434502

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

cut eliminationKnuth-Bendix completiondeduction moduloabstract canonical systemproof orderingautomated deduction and interactive theorem proving

Mathematics Subject Classification ID

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

Related Items (4)

Canonicity! ⋮ Resolution is cut-free ⋮ Regaining cut admissibility in deduction modulo using abstract completion ⋮ Axiom Directed Focusing

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