Theory Resolution_Sound

theory Resolution_Sound
imports Resolution CNF_Formulas_Sema
begin

(* there is one theory where we show Resolution completeness entirely without the relation to 
normal formulas. We haven't done the same for soundness, because we do not want too many theory files. *)

lemma Resolution_insert: "S ⊒ R ⟹ cnf_semantics π’œ S ⟹ cnf_semantics π’œ {R}"
by(induction  rule: Resolution.induct;
   clarsimp simp add: cnf_semantics_def clause_semantics_def lit_semantics_cases split: literal.splits;
   blast)

(* SchΓΆning's resolution lemma. We don't use it. *)
lemma "S ⊒ R ⟹ cnf_semantics π’œ S ⟷ cnf_semantics π’œ (R β–Ή S)"
  using Resolution_insert cnf_semantics_def by (metis insert_iff)

corollary Resolution_cnf_sound: assumes "S ⊒ β–‘" shows "Β¬ cnf_semantics π’œ S"
proof(rule notI)
  assume "cnf_semantics π’œ S"
  with Resolution_insert assms have "cnf_semantics π’œ {β–‘}" .
  thus False by(simp add: cnf_semantics_def clause_semantics_def)
qed

corollary Resolution_sound: 
  assumes rp: "cnf (nnf F) ⊒ β–‘"
  shows "Β¬ π’œ ⊨ F"
proof -
  from Resolution_cnf_sound rp have "Β¬ cnf_semantics π’œ (cnf (nnf F))" .
  hence "Β¬π’œ ⊨ nnf F" unfolding cnf_semantics[OF is_nnf_nnf] .
  thus ?thesis unfolding nnf_semantics .
qed

end