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)

• Theorem proving modulo
• Twenty years of rewriting logic
• A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
• Formalization of universal algebra in Agda
• Modular proof systems for partial functions with Evans equality
• The Formal System of Dijkstra and Scholten
• Orthogonality and Boolean Algebras for Deduction Modulo
• Embedding Deduction Modulo into a Prover
• Modular redundancy for theorem proving
• The MODPROF theorem prover
• Automated Reasoning
• Verification Modulo theories

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)