Nuprl Definition : full-omega

full-omega works on "integer formulas". It first puts the formula
into disjunctive-normal-form where each disjunct is collection
of "polynomial constraints" (a polynomial in the "atoms" of the formula
which is either =0 or >0).

Each set of polynomial constraints is "linearized" to (linear) 
"integer problem", set of linear forms =0 or >0.

omega is run on each of these problems, and if all the results are ff
then the formula is unsatisfiable. If any of the results are tt
then the formlua might be satisfiable, but is not guaranteed to be.
That is because we have not implemented Bill Pugh's "dark shadow" test.

However, for theorem proving, "semi decision" that can guarantees that
formula is unsatisfiable seems to be good enough.⋅

full-omega(fmla) ==
  eval dnf evalall(int_formula_dnf(fmla)) in
  ∨blet eqs,ineqs pcs-to-integer-problem(pc) 
    in case omega(eqs;ineqs) of inl(x) => tt inr(_) => ff;ff;dnf)

Definitions occuring in Statement :  omega: omega(eqs;ineqs) pcs-to-integer-problem: pcs-to-integer-problem(X) int_formula_dnf: int_formula_dnf(fmla) eager-accum: eager-accum(x,a.f[x; a];y;l) bor: p ∨bq evalall: evalall(t) callbyvalue: callbyvalue bfalse: ff btrue: tt spread: spread def decide: case of inl(x) => s[x] inr(y) => t[y]
Definitions occuring in definition :  callbyvalue: callbyvalue evalall: evalall(t) int_formula_dnf: int_formula_dnf(fmla) eager-accum: eager-accum(x,a.f[x; a];y;l) bor: p ∨bq spread: spread def pcs-to-integer-problem: pcs-to-integer-problem(X) decide: case of inl(x) => s[x] inr(y) => t[y] omega: omega(eqs;ineqs) btrue: tt bfalse: ff
FDL editor aliases :  full-omega

full-omega(fmla)  ==
    eval  dnf  =  evalall(int\_formula\_dnf(fmla))  in
    \mvee{}\msubb{}let  eqs,ineqs  =  pcs-to-integer-problem(pc) 
        in  case  omega(eqs;ineqs)  of  inl(x)  =>  tt  |  inr($_{}$)  =>  ff;ff;dnf)

Date html generated: 2017_09_29-PM-05_56_08
Last ObjectModification: 2017_06_01-PM-00_31_57

Theory : omega

Home Index