An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
From MaRDI portal
Publication:2864522
DOI10.1016/j.entcs.2006.11.037zbMath1277.68132OpenAlexW2056554620MaRDI QIDQ2864522
Cesare Tinelli, Clark Barrett, Igor Shikanian
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.037
Related Items
Reasoning about algebraic data types with abstractions, Efficiently solving quantified bit-vector formulas, Syntax-guided quantifier instantiation, Locality Results for Certain Extensions of Theories with Bridging Functions, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Rewrite-Based Satisfiability Procedures for Recursive Data Structures
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Abstract congruence closure
- An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Reasoning About Recursively Defined Data Structures
- An Efficient Unification Algorithm
- Automated Reasoning
- Computer Aided Verification
- Splitting on Demand in SAT Modulo Theories
- Logics in Artificial Intelligence
- Theorem Proving in Higher Order Logics