Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Combining Decision Procedures
Erschienen in: The Calculus of Computation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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?