def Validator.Formula.Clause.IsHorn {n : ℕ} (γ : Clause n) : Prop

Equations

• γ.IsHorn = (List.countP Validator.Formula.Literal.isPos γ ≤ 1)

@[implicit_reducible]

instance Validator.Formula.Clause.instDecidableIsHorn {n : ℕ} (γ : Clause n) : Decidable γ.IsHorn

Equations

• γ.instDecidableIsHorn = Validator.Formula.Clause.instDecidableIsHorn._aux_1✝ γ

structure Validator.Horn (n : ℕ) : Type

• vars : STRIPS.VarSet n
• empty : Bool
• unit_literals : Validator.Formula.PartialModel n
• clauses : Validator.Formula.CNF n
• horn_prop (γ : Validator.Formula.Clause n) : γ ∈ clauses self → γ.IsHorn
• clauses_prop (γ : Validator.Formula.Clause n) : γ ∈ clauses self → 2 ≤ List.length γ
• subset_vars (i : Fin n) : i ∈ (unit_literals self).vars ∪ (clauses self).vars → i ∈ vars self
• vars_prop : (unit_literals self).vars ∩ (clauses self).vars = ∅

def Validator.instDecidableEqHorn.decEq {n✝ : ℕ} (x✝ x✝¹ : Horn n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.instDecidableEqHorn {n✝ : ℕ} : DecidableEq (Horn n✝)

Equations

• Validator.instDecidableEqHorn = Validator.instDecidableEqHorn.decEq

@[implicit_reducible]

instance Validator.Horn.instFormula {n : ℕ} : Formula n (Horn n)

Equations

• Validator.Horn.instFormula = { vars := fun (φ : Validator.Horn n) => Validator.Horn.vars✝ φ, models := Validator.Horn.models✝, models_equiv_right := ⋯ }

@[implicit_reducible]

instance Validator.Horn.instTop {n : ℕ} : Formula.Top n (Horn n)

Equations

• Validator.Horn.instTop = { top := Validator.Horn.top✝, models_top := ⋯ }

@[implicit_reducible]

instance Validator.Horn.instBot {n : ℕ} : Formula.Bot n (Horn n)

Equations

• Validator.Horn.instBot = { bot := Validator.Horn.bot✝, vars_bot := ⋯, models_bot := ⋯ }

@[implicit_reducible]

instance Validator.Horn.instConsistency {n : ℕ} : Formula.Consistency n (Horn n)

Equations

• Validator.Horn.instConsistency = { consistent := fun (φ : Validator.Horn n) => decide ¬Validator.Horn.empty✝ φ = true, consistent_iff := ⋯ }

@[implicit_reducible]

instance Validator.Horn.instClausalEntailment {n : ℕ} : Formula.ClausalEntailment n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.Horn.instSententialEntailment {n : ℕ} : Formula.SententialEntailment n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.Horn.instBoundedConjuction {n : ℕ} : Formula.BoundedConjuction n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.Horn.instOfPartialModel {n : ℕ} : Formula.OfPartialModel n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.Horn.instImplicant {n : ℕ} : Formula.Implicant n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.Horn.instRename {n : ℕ} : Formula.Rename n (Horn n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.Horn.instToCNF {n : ℕ} : Formula.ToCNF n (Horn n)

Equations

• Validator.Horn.instToCNF = { toCNF := Validator.Horn.toCNF✝, models_toCNF := ⋯ }

def Validator.Horn.fromCNF {n : ℕ} (φ : Formula.CNF n) : Option (Horn n)

Translate the given CNF formula to a Horn-formula. Returns none if the CNF-formula is not a Horn-formula.

Equations

• Validator.Horn.fromCNF φ = List.foldrM Validator.Horn.insert'✝ Validator.Horn.top✝ φ

theorem Validator.Horn.vars_fromCNF {n : ℕ} {φ : Formula.CNF n} {ψ : Horn n} : fromCNF φ = some ψ → Formula.vars ψ ⊆ φ.vars

theorem Validator.Horn.models_fromCNF {n : ℕ} {φ : Formula.CNF n} {ψ : Horn n} : fromCNF φ = some ψ → Formula.models ψ = φ.models