Practical Decision
Having practical decision procedures for classes of logical formulas is of considerable interest for program verification and circuit verification. Pure Boolean logical formulas are usually decided using SAT-solving techniques based on the DPLL algorithm. Conjunctive formulas over linear real or rational arithmetic can be decided using the simplex algorithm, formulas in linear integer arithmetic (Presburger arithmetic) can be decided using Cooper's algorithm or William Pugh's Omega test. Formulas with negations, conjunctions and disjunctions combine the difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using SMT-solving technique, which combine SAT-solving with decision procedures for conjunctions and propagation techniques. Real polynomial arithmetic, also known as the theory of real closed fields, is decidable, for instance using the cylindrical algebraic decomposition; unfortunately the complexity of that algorithm is excessive for most practical uses.
A leading scientific conference in this field is Computer Aided Verification.
Read more about this topic: Decision Problem
Famous quotes containing the words practical and/or decision:
“After all, the practical reason why, when the power is once in the hands of the people, a majority are permitted, and for a long period continue, to rule is not because they are most likely to be in the right, nor because this seems fairest to the minority, but because they are physically the strongest. But a government in which the majority rule in all cases cannot be based on justice, even as far as men understand it.”
—Henry David Thoreau (1817–1862)
“Will mankind never learn that policy is not morality,—that it never secures any moral right, but considers merely what is expedient? chooses the available candidate,—who is invariably the devil,—and what right have his constituents to be surprised, because the devil does not behave like an angel of light? What is wanted is men, not of policy, but of probity,—who recognize a higher law than the Constitution, or the decision of the majority.”
—Henry David Thoreau (1817–1862)