Theorem Proving Modulo Based on Boolean Equational Procedures

DOI10.1007/978-3-540-78913-0_25MaRDI QIDQ3498425zbMATH OpenOpenAlexFDO

Authors Camilo Rocha, José Meseguer

Publication date 15 May 2008

Published in Relations and Kleene Algebra in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78913-0_25

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Theorem proving modulo
• Automated Reasoning
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Experimenting with deduction modulo
• Orthogonality and Boolean Algebras for Deduction Modulo

Cited in

(12)

• Twenty years of rewriting logic
• scientific article; zbMATH DE number 1538015 (Why is no real title available?)
• Formalization of universal algebra in Agda
• Embedding Deduction Modulo into a Prover
• The Formal System of Dijkstra and Scholten
• Verification Modulo theories
• Automated Reasoning
• Orthogonality and Boolean Algebras for Deduction Modulo
• scientific article; zbMATH DE number 1765692 (Why is no real title available?)
• Modular proof systems for partial functions with Evans equality
• Theorem proving modulo
• A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems

Describes a project that uses

Uses Software

• Maude

This page was built for publication: Theorem Proving Modulo Based on Boolean Equational Procedures

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