On Constructive Cut Admissibility in Deduction Modulo

DOI10.1007/978-3-540-74464-1_3zbMATH Open1178.03021OpenAlexW1607964314MaRDI QIDQ3612434FDOQ3612434

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

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

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)

Cited In (9)

• Title not available (Why is that?)
• 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
• A Semantic Completeness Proof for TaMeD
• Cut Elimination in Deduction Modulo by 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)