Rewrite-based satisfiability procedures for recursive data structures

DOI10.1016/J.ENTCS.2006.11.039MaRDI QIDQ2864524zbMATH OpenOpenAlexFDO

Authors 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

Data structures (68P05)

Recommendations

• Rewrite-based decision procedures
• New results on rewrite-based satisfiability procedures
• Frontiers of Combining Systems
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Mechanizing Mathematical Reasoning

Cites work

• A rewriting approach to satisfiability procedures.
• Abstract congruence closure
• An abstract decision procedure for satisfiability in the theory of recursive data types
• Automated Reasoning
• Congruence closure with integer offsets
• Frontiers of Combining Systems
• Paramodulation-based theorem proving
• Reasoning About Recursively Defined Data Structures
• Term Rewriting and All That

Cited in

(14)

• An abstract decision procedure for satisfiability in the theory of recursive data types
• Canonical ground Horn theories
• Interpolation systems for ground proofs in automated deduction: a survey
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• On deciding satisfiability by theorem proving with speculative inferences
• New results on rewrite-based satisfiability procedures
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Theory decision by decomposition
• A rewriting approach to satisfiability procedures.
• Politeness for the theory of algebraic datatypes
• Syntax-guided rewrite rule enumeration for SMT solvers
• On interpolation in automated theorem proving
• Rewrite-based decision procedures
• Polite combination of algebraic datatypes

This page was built for publication: Rewrite-based satisfiability procedures for recursive data structures

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