Embedding Deduction Modulo into a Prover

DOI10.1007/978-3-642-15205-4_15MaRDI QIDQ3586040zbMATH OpenOpenAlexFDO

Authors Guillaume Burel

Publication date 3 September 2010

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-15205-4_15

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 2174387
• Theorem Proving Modulo Based on Boolean Equational Procedures
• Equational theorem proving modulo
• Extensional proofs in a propositional logic modulo isomorphisms
• Combining deduction modulo and logics of fixed-point definitions
• scientific article; zbMATH DE number 1765692
• On the completeness of modular proof systems
• A modal provability logic of explicit and implicit proofs
• scientific article; zbMATH DE number 1538015
• Proving equational and inductive theorems by completion and embedding techniques

Cited in

(13)

• Theorem proving modulo
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Regaining cut admissibility in deduction modulo using abstract completion
• Restricted combinatory unification
• Tactics for Reasoning Modulo AC in Coq
• CTL model checking in deduction modulo
• On Constructive Cut Admissibility in Deduction Modulo
• Automating theories in intuitionistic logic
• scientific article; zbMATH DE number 1538015 (Why is no real title available?)
• scientific article; zbMATH DE number 1765692 (Why is no real title available?)
• scientific article; zbMATH DE number 2086373 (Why is no real title available?)
• Experimenting with deduction modulo
• Automated Reasoning

This page was built for publication: Embedding Deduction Modulo into a Prover

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