Rewrite-based satisfiability procedures for recursive data structures
From MaRDI portal
Publication:2864524
DOI10.1016/J.ENTCS.2006.11.039zbMATH Open1277.68239OpenAlexW2027211529MaRDI QIDQ2864524FDOQ2864524
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
Recommendations
Cites Work
- Term Rewriting and All That
- A rewriting approach to satisfiability procedures.
- Paramodulation-based theorem proving
- Frontiers of Combining Systems
- Reasoning About Recursively Defined Data Structures
- Congruence closure with integer offsets
- Abstract congruence closure
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Automated Reasoning
Cited In (14)
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Canonical ground Horn theories
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Interpolation systems for ground proofs in automated deduction: a survey
- New results on rewrite-based satisfiability procedures
- On deciding satisfiability by theorem proving with speculative inferences
- 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)
