Nuprl Definition : omega

omega works on an "integer problem" that is set of equality constraints
and set of inequality constraints. It start by normalizing the constraints.
Then it repeats the "omega_step". On each step, either the number of 
equality constraints decreases, or the dimension of the problem (the number
of variables) decreases. Thus the algorithm terminates.

Each step preserves satisfiablity of the constraints, meaning that if
the resulting problem is unsatisfiable then the original problem is
unsatisfiable. Because we have not implemented Bill Pugh's "dark shadow"
test, the reverse is not true in general (the reduced problem could be
satisfiable even though the original problem was unsatisfiable).⋅

omega(eqs;ineqs) ==  let s ⟵ omega_start(eqs;ineqs) in rep_int_constraint_step(λp.omega_step(p);s)

Definitions occuring in Statement :  omega_start: omega_start(eqs;ineqs) omega_step: omega_step(p) rep_int_constraint_step: rep_int_constraint_step(f;p) callbyvalueall: callbyvalueall lambda: λx.A[x]
Definitions occuring in definition :  callbyvalueall: callbyvalueall omega_start: omega_start(eqs;ineqs) rep_int_constraint_step: rep_int_constraint_step(f;p) lambda: λx.A[x] omega_step: omega_step(p)
FDL editor aliases :  omega

omega(eqs;ineqs)  ==    let  s  \mleftarrow{}{}  omega\_start(eqs;ineqs)  in  rep\_int\_constraint\_step(\mlambda{}\_step(p);s)

Date html generated: 2016_07_08-PM-04_48_47
Last ObjectModification: 2016_02_29-PM-06_24_56

Theory : omega

Home Index