An Efficient Decision Procedure for Functional Decomposable Theories Based on Dual Constraints
From MaRDI portal
Publication:5191405
DOI10.1007/978-3-642-03251-6_3zbMath1248.03019MaRDI QIDQ5191405
Publication date: 6 August 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-03251-6_3
03B25: Decidability of theories and sets of sentences
03C07: Basic properties of first-order languages and structures
Cites Work
- Unnamed Item
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- Expressiveness of full first-order constraints in the algebra of finite or infinite trees
- A decision procedure for term algebras with queues
- Theory of finite or infinite trees revisited
- Principles of Constraint Programming
- Extension of First-Order Theories into Trees
- Decomposable theories
- Frontiers of Combining Systems
- A Full First-Order Constraint Solver for Decomposable Theories