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:
“I favor the policy of economy, not because I wish to save money, but because I wish to save people. The men and women of this country who toil are the ones who bear the cost of the Government. Every dollar that we carelessly waste means that their life will be so much the more meager. Every dollar that we prudently save means that their life will be so much the more abundant. Economy is idealism in its most practical terms.”
—Calvin Coolidge (1872–1933)
“Our decision about energy will test the character of the American people and the ability of the President and the Congress to govern this nation. This difficult effort will be the “moral equivalent of war,” except that we will be uniting our efforts to build and not to destroy.”
—Jimmy Carter (James Earl Carter, Jr.)