# Theory Clausal_Calculus

(*  Title:       Clausal Calculi
Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2020
*)

section ‹Clausal Calculi›

theory Clausal_Calculus
imports
Ordered_Resolution_Prover.Unordered_Ground_Resolution
Soundness
Standard_Redundancy_Criterion
begin

text ‹Various results about consequence relations, counterexample-reducing inference systems, and
the standard redundancy criteria are specialized and customized for clauses as opposed to arbitrary
formulas.›

subsection ‹Setup›

text ‹To avoid confusion, we use the symbol ⊫› (with or without subscripts) for the ``models''
and entailment relations on clauses and ⊨› for the abstract concept of consequence.›

abbreviation true_lit_thick :: "'a interp  'a literal  bool" (infix "⊫l" 50) where
"I ⊫l L  I ⊨l L"

abbreviation true_cls_thick :: "'a interp  'a clause  bool" (infix "" 50) where
"I  C  I  C"

abbreviation true_clss_thick :: "'a interp  'a clause set  bool" (infix "⊫s" 50) where
"I ⊫s 𝒞  I ⊨s 𝒞"

abbreviation true_cls_mset_thick :: "'a interp  'a clause multiset  bool" (infix "⊫m" 50) where
"I ⊫m 𝒞  I ⊨m 𝒞"

no_notation true_lit (infix "⊨l" 50)
no_notation true_cls (infix "" 50)
no_notation true_clss (infix "⊨s" 50)
no_notation true_cls_mset (infix "⊨m" 50)

subsection ‹Consequence Relation›

abbreviation entails_clss :: "'a clause set  'a clause set  bool" (infix "⊫e" 50) where
"N1 ⊫e N2  I. I ⊫s N1  I ⊫s N2"

lemma entails_iff_unsatisfiable_single:
"CC ⊫e {E}  ¬ satisfiable (CC  {{#- L#} |L. L ∈# E})" (is "_  _ (_  ?NegD)")
proof
assume c_ent_e: "CC ⊫e {E}"
have "¬ I ⊫s CC  ?NegD" for I
using c_ent_e[rule_format, of I]
unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj
by (fastforce simp: ball_Un is_pos_neg_not_is_pos)
then show "¬ satisfiable (CC  ?NegD)"
by auto
next
assume "¬ satisfiable (CC  ?NegD)"
then have "¬ I ⊫s CC  ?NegD" for I
by auto
then show "CC ⊫e {E}"
unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj
by (fastforce simp: ball_Un is_pos_neg_not_is_pos)
qed

lemma entails_iff_unsatisfiable:
"CC ⊫e EE  (E  EE. ¬ satisfiable (CC  {{#- L#} |L. L ∈# E}))" (is "?lhs = ?rhs")
proof -
have "?lhs  (E  EE. CC ⊫e {E})"
unfolding true_clss_def by auto
also have "...  ?rhs"
unfolding entails_iff_unsatisfiable_single by auto
finally show ?thesis
.
qed

interpretation consequence_relation "{{#}}" "(⊫e)"
proof
fix N2 N1 :: "'a clause set"
assume "C  N2. N1 ⊫e {C}"
then show "N1 ⊫e N2"
unfolding true_clss_singleton by (simp add: true_clss_def)
qed (auto intro: true_clss_mono)

interpretation concl_compact_consequence_relation "{{#}} :: ('a :: wellorder) clause set" "(⊫e)"
proof
fix CC EE :: "'a clause set"
assume
fin_e: "finite EE" and
c_ent_e: "CC ⊫e EE"

have "E  EE. ¬ satisfiable (CC  {{#- L#} |L. L ∈# E})"
using c_ent_e[unfolded entails_iff_unsatisfiable] .
then have "E  EE. DD  CC  {{#- L#} |L. L ∈# E}. finite DD  ¬ satisfiable DD"
by (subst (asm) clausal_logic_compact)
then obtain DD_of where
d_of: "E  EE. DD_of E  CC  {{#- L#} |L. L ∈# E}  finite (DD_of E)
¬ satisfiable (DD_of E)"
by moura

define CC' where
"CC' = (E  EE. DD_of E - {{#- L#} |L. L ∈# E})"

have "CC'  CC"
unfolding CC'_def using d_of by auto
moreover have c'_fin: "finite CC'"
unfolding CC'_def using d_of fin_e by blast
moreover have "CC' ⊫e EE"
unfolding entails_iff_unsatisfiable
proof
fix E
assume e_in: "E  EE"

have "DD_of E  CC'  {{#- L#} |L. L ∈# E}"
using e_in d_of unfolding CC'_def by auto
moreover have "¬ satisfiable (DD_of E)"
using e_in d_of by auto
ultimately show "¬ satisfiable (CC'  {{#- L#} |L. L ∈# E})"
by (rule unsatisfiable_mono[of "DD_of E"])
qed
ultimately show "CC'  CC. finite CC'  CC' ⊫e EE"
by blast
qed

subsection ‹Counterexample-Reducing Inference Systems›

definition clss_of_interp :: "'a set  'a literal multiset set" where
"clss_of_interp I = {{#(if A  I then Pos else Neg) A#} |A. True}"

lemma true_clss_of_interp_iff_equal[simp]: "J ⊫s clss_of_interp I  J = I"
unfolding clss_of_interp_def true_clss_def true_cls_def true_lit_def by force

lemma entails_iff_models[simp]: "clss_of_interp I ⊫e CC  I ⊫s CC"
by simp

locale clausal_counterex_reducing_inference_system = inference_system Inf
for Inf :: "('a :: wellorder) clause inference set" +
fixes J_of :: "'a clause set  'a interp"
assumes clausal_Inf_counterex_reducing:
"{#}  N  D  N  ¬ J_of N  D  (C. C  N  ¬ J_of N  C  D  C)
ι  Inf. prems_of ι  []  main_prem_of ι = D  set (side_prems_of ι)  N
J_of N ⊫s set (side_prems_of ι)  ¬ J_of N  concl_of ι  concl_of ι < D"
begin

abbreviation I_of :: "'a clause set  'a clause set" where
"I_of N  clss_of_interp (J_of N)"

lemma Inf_counterex_reducing:
assumes
bot_ni_n: "N  {{#}} = {}" and
d_in_n: "D  N" and
n_ent_d: "¬ I_of N ⊫e {D}" and
d_min: "C. C  N  ¬ I_of N ⊫e {C}  D  C"
shows "ι  Inf. prems_of ι  []  main_prem_of ι = D  set (side_prems_of ι)  N
I_of N ⊫e set (side_prems_of ι)  ¬ I_of N ⊫e {concl_of ι}  concl_of ι < D"
using bot_ni_n clausal_Inf_counterex_reducing d_in_n d_min n_ent_d by auto

sublocale counterex_reducing_inference_system "{{#}}" "(⊫e)" Inf I_of
"(<) :: 'a clause  'a clause  bool"
using Inf_counterex_reducing

end

subsection ‹Counterexample-Reducing Calculi Equipped with a Standard Redundancy Criterion›

locale clausal_counterex_reducing_calculus_with_standard_redundancy =
calculus_with_standard_redundancy Inf "{{#}}" "(⊫e)" "(<) :: 'a clause  'a clause  bool" +
clausal_counterex_reducing_inference_system Inf J_of
for
Inf :: "('a :: wellorder) clause inference set" and
J_of :: "'a clause set  'a set"
begin

sublocale counterex_reducing_calculus_with_standard_inferance_redundancy "{{#}}" Inf "(⊫e)" Red_I
Red_F I_of "(<) :: 'a clause  'a clause  bool"
proof unfold_locales
fix C D :: "'a clause"
show "C  D  C < D  D < C"
by fastforce
qed

lemma clausal_saturated_model: "saturated N  {#}  N  J_of N ⊫s N"