A Semantic Completeness Proof for TaMeD

DOI10.1007/11916277_12MaRDI QIDQ5387891zbMATH OpenOpenAlexFDO

Authors Richard Bonichon, Olivier Hermant

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11916277_12

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• On Constructive Cut Admissibility in Deduction Modulo
• Automated Reasoning
• Regaining cut admissibility in deduction modulo using abstract completion
• Theorem proving modulo
• Experimenting with deduction modulo

Cited in

(4)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Regaining cut admissibility in deduction modulo using abstract completion
• Experimenting with deduction modulo
• Resolution is cut-free

This page was built for publication: A Semantic Completeness Proof for TaMeD

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