Rewrite-Based Satisfiability Procedures for Recursive Data Structures

DOI10.1016/j.entcs.2006.11.039zbMath1277.68239OpenAlexW2027211529MaRDI QIDQ2864524

Maria Paola Bonacina, Mnacho Echenim

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.11.039

zbMATH Keywords

recursive data structuresrewrite-based inference systems

Mathematics Subject Classification ID

Related Items (9)

Interpolation systems for ground proofs in automated deduction: a survey ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Canonical Ground Horn Theories ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Theory decision by decomposition ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes ⋮ Rewrite-Based Decision Procedures ⋮ On interpolation in automated theorem proving

Cites Work

• Unnamed Item
• Unnamed Item
• A rewriting approach to satisfiability procedures.
• Abstract congruence closure
• An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
• Reasoning About Recursively Defined Data Structures
• Term Rewriting and All That
• Automated Reasoning
• Frontiers of Combining Systems

This page was built for publication: Rewrite-Based Satisfiability Procedures for Recursive Data Structures