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 (v : ) :
omega.clause → Prop

holds v c := clause c holds under valuation v

Equations
def omega.clause.sat (c : omega.clause) :
Prop

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

Equations
def omega.clause.unsat (c : omega.clause) :
Prop

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

Equations

append two clauses by elementwise appending

Equations
def omega.clauses.sat (cs : list omega.clause) :
Prop

There exists a satisfiable clause c in argument

Equations

There is no satisfiable clause c in argument

Equations