Advertisement
Published in:
2007 | OriginalPaper | Chapter
Combining Decision Procedures
Published in: The Calculus of Computation
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Chapters 7–9 consider decision procedures for theories that each formalize just one data type. Yet almost all formulae in Chapter 5 are formulae of union theories. For example, many assert facts in
T
ℚ
∪
T
A
about arrays of integers indexed by integers. Additionally, the decision procedure for the array property fragment of
T
A
ℚ
that we discuss in Chapter 11 requires a procedure for the quantifier-free fragment of
T
ℚ
∪
T
A
. Can we reuse the decision procedures of Chapters 7–9 to decide satisfiability of formulae in union theories, or must we invent a new procedure for each combination?