Nuprl Definition : full-omega
full-omega works on "integer formulas". It first puts the formula
into a disjunctive-normal-form where each disjunct is a 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 a (linear)
"integer problem", a 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, a "semi decision" that can guarantees that
a formula is unsatisfiable seems to be good enough.⋅
full-omega(fmla) ==
eval dnf = evalall(int_formula_dnf(fmla)) in
eager-accum(sat,pc.sat
∨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 b 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 b of inl(x) => s[x] | inr(y) => t[y],
omega: omega(eqs;ineqs),
btrue: tt,
bfalse: ff
FDL editor aliases :
full-omega
Latex:
full-omega(fmla) ==
eval dnf = evalall(int\_formula\_dnf(fmla)) in
eager-accum(sat,pc.sat
\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