### Nuprl Definition : omega

`omega works on an "integer problem" that is a set of equality constraints`
`and a 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

Latex:
omega(eqs;ineqs)  ==    let  s  \mleftarrow{}{}  omega\_start(eqs;ineqs)  in  rep\_int\_constraint\_step(\mlambda{}p.omega\_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