On Constructive Cut Admissibility in Deduction Modulo

DOI10.1007/978-3-540-74464-1_3MaRDI QIDQ3612434zbMATH OpenOpenAlexFDO

Authors Richard Bonichon, Olivier Hermant

Publication date 10 March 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74464-1_3

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Recommendations

• Regaining cut admissibility in deduction modulo using abstract completion
• Constructive Dedekind cuts
• Cut Elimination in Deduction Modulo by Abstract Completion
• Admissibility of cut in congruent modal logics
• Modular Cut-Elimination: Finding Proofs or Counterexamples
• Admissibility of cut in coalgebraic logics
• scientific article; zbMATH DE number 7599492
• The arithmetic of cuts in models of arithmetic
• Cut Elimination in the Presence of Axioms
• Embedding Deduction Modulo into a Prover

Cited in

(9)

• A Semantic Completeness Proof for TaMeD
• Cut Elimination in Deduction Modulo by Abstract Completion
• scientific article; zbMATH DE number 1538009 (Why is no real title available?)
• Automating theories in intuitionistic logic
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Algorithmic Equality in Heyting Arithmetic Modulo
• Resolution is cut-free
• Theorem proving modulo
• Regaining cut admissibility in deduction modulo using abstract completion

This page was built for publication: On Constructive Cut Admissibility in Deduction Modulo

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