An abstract decision procedure for satisfiability in the theory of recursive data types
From MaRDI portal
Publication:2864522
DOI10.1016/J.ENTCS.2006.11.037zbMATH Open1277.68132OpenAlexW2056554620MaRDI QIDQ2864522FDOQ2864522
Authors: Clark Barrett, Igor Shikanian, Cesare Tinelli 
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
Recommendations
- An abstract decision procedure for a theory of inductive data types.
- Decision procedures for algebraic data types with abstractions
- A decision procedure for (co)datatypes in SMT solvers
- A decision procedure for (co)datatypes in SMT solvers
- Rewrite-based satisfiability procedures for recursive data structures
- scientific article
- Decidability properties of recursive types.
- A coinduction principle for recursive data types based on bisimulation
- Deterministic and nondeterministic computation, and horn programs, on abstract data types
- scientific article; zbMATH DE number 3936490
Cites Work
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- An Efficient Unification Algorithm
- Splitting on Demand in SAT Modulo Theories
- Fast Decision Procedures Based on Congruence Closure
- Title not available (Why is that?)
- A practical approach to partial functions in CVC Lite
- Logics in Artificial Intelligence
- Reasoning About Recursively Defined Data Structures
- Computer Aided Verification
- Abstract congruence closure
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Automated Reasoning
- Theorem Proving in Higher Order Logics
Cited In (9)
- Locality Results for Certain Extensions of Theories with Bridging Functions
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Abstract GSOS rules and a modular treatment of recursive definitions
- Syntax-guided quantifier instantiation
- Decision procedures for algebraic data types with abstractions
- Efficiently solving quantified bit-vector formulas
- An abstract decision procedure for a theory of inductive data types.
- Reasoning about algebraic data types with abstractions
- Rewrite-based satisfiability procedures for recursive data structures
Uses Software
This page was built for publication: An abstract decision procedure for satisfiability in the theory of recursive data types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864522)
