mathlib documentation

tactic.omega.clause

def omega.clause  :
Type

(([t₁,...tₘ],[s₁,...,sₙ]) : clause) encodes the constraints 0 = ⟦t₁⟧ ∧ ... ∧ 0 = ⟦tₘ⟧ ∧ 0 ≤ ⟦s₁⟧ ∧ ... ∧ 0 ≤ ⟦sₙ⟧, where ⟦t⟧ is the value of (t : term).

Equations
def omega.clause.holds  :
()omega.clause → Prop

holds v c := clause c holds under valuation v

Equations
def omega.clause.sat  :
omega.clause → Prop

sat c := there exists a valuation v under which c holds

Equations
def omega.clause.unsat  :
omega.clause → Prop

unsat c := there is no valuation v under which c holds

Equations

append two clauses by elementwise appending

Equations

There exists a satisfiable clause c in argument

Equations

There is no satisfiable clause c in argument

Equations