Theory "CNF"

Parents     partitioning

Signature

Constant Type
clause_dom :α clause -> α -> bool
colouring :((α -> bool) -> bool) -> α formula -> bool
consistent_tvsal :(α -> β) # α formula # β formula -> bool
covering_tvsals :((α -> β) -> bool) # α formula # β formula -> bool
formula_dom :α formula -> α -> bool
image_clause :(β -> α) -> β clause -> α clause
image_formula :(β -> α) -> β formula -> α formula
model :α formula
models_clause :α clause -> α formula
models_formula :α clause -> α formula -> bool

Definitions

model_def
|- ∀M. model M ⇔ ∀x. (x,T) ∉ M ∨ (x,F) ∉ M
models_clause_def
|- ∀M c. models_clause M c ⇔ M ∩ c ≠ ∅
models_formula_def
|- ∀M phi. models_formula M phi ⇔ ∀c. c ∈ phi ⇒ models_clause M c
image_clause_def
|- ∀f c. image_clause f c = IMAGE (λl. (f (FST l),SND l)) c
image_formula_def
|- ∀f phi. image_formula f phi = IMAGE (image_clause f) phi
consistent_tvsal_def
|- ∀tvsal phi phi'.
     consistent_tvsal (tvsal,phi,phi') ⇔ image_formula tvsal phi ⊆ phi'
covering_tvsals_def
|- ∀tvsals phi phi'.
     covering_tvsals (tvsals,phi,phi') ⇔
     phi' ⊆ BIGUNION {image_formula tvsal phi | tvsal ∈ tvsals}
clause_dom_def
|- ∀c. clause_dom c = {x | ∃bv. (x,bv) ∈ c}
formula_dom_def
|- ∀phi. formula_dom phi = BIGUNION {clause_dom c | c ∈ phi}
colouring_def
|- ∀P phi.
     colouring P phi ⇔
     ∀p x y.
       p ∈ P ∧ x ∈ p ∧ y ∈ p ⇒
       (x = y) ∨ ∀c. c ∈ phi ⇒ x ∉ clause_dom c ∨ y ∉ clause_dom c