2007 | OriginalPaper | Buchkapitel
Quantifier-Free Linear Arithmetic
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
This chapter considers satisfiability in the quantifier-free fragment of the theory of rationals
T
ℚ
. Addressing this fragment is motivated by two observations. First, program verification typically requires just considering formulae from the quantifier-free fragments of theories such as
T
ℚ
. Second, deciding satisfiability in the full theory of
T
ℚ
is computationally expensive, while deciding satisfiability in just the quantifier-free fragment of
T
ℚ
is fast in practice when using, for example, the
simplex method
for
linear programming
.