Theory Ordered_Ground_Resolution
section ‹Ground Ordered Resolution Calculus with Selection›
theory Ordered_Ground_Resolution
imports Inference_System Ground_Resolution_Model
begin
text ‹
Ordered ground resolution with selection is the second inference system studied in Section~3
(``Standard Resolution'') of Bachmair and Ganzinger's chapter.
›
subsection ‹Inference Rule›
text ‹
Ordered ground resolution consists of a single rule, called ‹ord_resolve› below. Like
‹unord_resolve›, the rule is sound and counterexample-reducing. In addition, it is reductive.
›
context ground_resolution_with_selection
begin
text ‹
The following inductive definition corresponds to Figure 2.
›
definition maximal_wrt :: "'a ⇒ 'a literal multiset ⇒ bool" where
"maximal_wrt A DA ⟷ DA = {#} ∨ A = Max (atms_of DA)"
definition strictly_maximal_wrt :: "'a ⇒ 'a literal multiset ⇒ bool" where
"strictly_maximal_wrt A CA ⟷ (∀B ∈ atms_of CA. B < A)"
inductive eligible :: "'a list ⇒ 'a clause ⇒ bool" where
eligible: "(S DA = negs (mset As)) ∨ (S DA = {#} ∧ length As = 1 ∧ maximal_wrt (As ! 0) DA) ⟹
eligible As DA"
lemma "(S DA = negs (mset As) ∨ S DA = {#} ∧ length As = 1 ∧ maximal_wrt (As ! 0) DA) ⟷
eligible As DA"
using eligible.intros ground_resolution_with_selection.eligible.cases ground_resolution_with_selection_axioms by blast
inductive
ord_resolve :: "'a clause list ⇒ 'a clause ⇒ 'a multiset list ⇒ 'a list ⇒ 'a clause ⇒ bool"
where
ord_resolve:
"length CAs = n ⟹
length Cs = n ⟹
length AAs = n ⟹
length As = n ⟹
n ≠ 0 ⟹
(∀i < n. CAs ! i = Cs ! i + poss (AAs ! i)) ⟹
(∀i < n. AAs ! i ≠ {#}) ⟹
(∀i < n. ∀A ∈# AAs ! i. A = As ! i) ⟹
eligible As (D + negs (mset As)) ⟹
(∀i < n. strictly_maximal_wrt (As ! i) (Cs ! i)) ⟹
(∀i < n. S (CAs ! i) = {#}) ⟹
ord_resolve CAs (D + negs (mset As)) AAs As (∑⇩# (mset Cs) + D)"
lemma ord_resolve_sound:
assumes
res_e: "ord_resolve CAs DA AAs As E" and
cc_true: "I ⊨m mset CAs" and
d_true: "I ⊨ DA"
shows "I ⊨ E"
using res_e
proof (cases rule: ord_resolve.cases)
case (ord_resolve n Cs D)
note DA = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
as_len = this(6) and cas = this(8) and aas_ne = this(9) and a_eq = this(10)
show ?thesis
proof (cases "∀A ∈ set As. A ∈ I")
case True
then have "¬ I ⊨ negs (mset As)"
unfolding true_cls_def by fastforce
then have "I ⊨ D"
using d_true DA by fast
then show ?thesis
unfolding e by blast
next
case False
then obtain i where
a_in_aa: "i < n" and
a_false: "As ! i ∉ I"
using cas_len as_len by (metis in_set_conv_nth)
have "¬ I ⊨ poss (AAs ! i)"
using a_false a_eq aas_ne a_in_aa unfolding true_cls_def by auto
moreover have "I ⊨ CAs ! i"
using a_in_aa cc_true unfolding true_cls_mset_def using cas_len by auto
ultimately have "I ⊨ Cs ! i"
using cas a_in_aa by auto
then show ?thesis
using a_in_aa cs_len unfolding e true_cls_def
by (meson in_Union_mset_iff nth_mem_mset union_iff)
qed
qed
lemma filter_neg_atm_of_S: "{#Neg (atm_of L). L ∈# S C#} = S C"
by (simp add: S_selects_neg_lits)
text ‹
This corresponds to Lemma 3.13:
›
lemma ord_resolve_reductive:
assumes "ord_resolve CAs DA AAs As E"
shows "E < DA"
using assms
proof (cases rule: ord_resolve.cases)
case (ord_resolve n Cs D)
note DA = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
ai_len = this(6) and nz = this(7) and cas = this(8) and maxim = this(12)
show ?thesis
proof (cases "∑⇩# (mset Cs) = {#}")
case True
have "negs (mset As) ≠ {#}"
using nz ai_len by auto
then show ?thesis
unfolding True e DA by auto
next
case False
define max_A_of_Cs where
"max_A_of_Cs = Max (atms_of (∑⇩# (mset Cs)))"
have
mc_in: "max_A_of_Cs ∈ atms_of (∑⇩# (mset Cs))" and
mc_max: "⋀B. B ∈ atms_of (∑⇩# (mset Cs)) ⟹ B ≤ max_A_of_Cs"
using max_A_of_Cs_def False by auto
then have "∃C_max ∈ set Cs. max_A_of_Cs ∈ atms_of (C_max)"
by (metis atm_imp_pos_or_neg_lit in_Union_mset_iff neg_lit_in_atms_of pos_lit_in_atms_of
set_mset_mset)
then obtain max_i where
cm_in_cas: "max_i < length CAs" and
mc_in_cm: "max_A_of_Cs ∈ atms_of (Cs ! max_i)"
using in_set_conv_nth[of _ CAs] by (metis cas_len cs_len in_set_conv_nth)
define CA_max where "CA_max = CAs ! max_i"
define A_max where "A_max = As ! max_i"
define C_max where "C_max = Cs ! max_i"
have mc_lt_ma: "max_A_of_Cs < A_max"
using maxim cm_in_cas mc_in_cm cas_len unfolding strictly_maximal_wrt_def A_max_def by auto
then have ucas_ne_neg_aa: "∑⇩# (mset Cs) ≠ negs (mset As)"
using mc_in mc_max mc_lt_ma cm_in_cas cas_len ai_len unfolding A_max_def
by (metis atms_of_negs nth_mem set_mset_mset leD)
moreover have ucas_lt_ma: "∀B ∈ atms_of (∑⇩# (mset Cs)). B < A_max"
using mc_max mc_lt_ma by fastforce
moreover have "¬ Neg A_max ∈# ∑⇩# (mset Cs)"
using ucas_lt_ma neg_lit_in_atms_of[of A_max "∑⇩# (mset Cs)"] by auto
moreover have "Neg A_max ∈# negs (mset As)"
using cm_in_cas cas_len ai_len A_max_def by auto
ultimately have "∑⇩# (mset Cs) < negs (mset As)"
unfolding less_multiset⇩H⇩O
by (metis (no_types) atms_less_eq_imp_lit_less_eq_neg count_greater_zero_iff
count_inI le_imp_less_or_eq less_imp_not_less not_le)
then show ?thesis
unfolding e DA by auto
qed
qed
text ‹
This corresponds to Theorem 3.15:
›
theorem ord_resolve_counterex_reducing:
assumes
ec_ni_n: "{#} ∉ N" and
d_in_n: "DA ∈ N" and
d_cex: "¬ INTERP N ⊨ DA" and
d_min: "⋀C. C ∈ N ⟹ ¬ INTERP N ⊨ C ⟹ DA ≤ C"
obtains CAs AAs As E where
"set CAs ⊆ N"
"INTERP N ⊨m mset CAs"
"⋀CA. CA ∈ set CAs ⟹ productive N CA"
"ord_resolve CAs DA AAs As E"
"¬ INTERP N ⊨ E"
"E < DA"
proof -
have d_ne: "DA ≠ {#}"
using d_in_n ec_ni_n by blast
have "∃As. As ≠ [] ∧ negs (mset As) ≤# DA ∧ eligible As DA"
proof (cases "S DA = {#}")
assume s_d_e: "S DA = {#}"
define A where "A = Max (atms_of DA)"
define As where "As = [A]"
define D where "D = DA-{#Neg A #}"
have na_in_d: "Neg A ∈# DA"
unfolding A_def using s_d_e d_ne d_in_n d_cex d_min
by (metis Max_in_lits Max_lit_eq_pos_or_neg_Max_atm max_pos_imp_Interp Interp_imp_INTERP)
then have das: "DA = D + negs (mset As)"
unfolding D_def As_def by auto
moreover from na_in_d have "negs (mset As) ⊆# DA"
by (simp add: As_def)
moreover have hd: "As ! 0 = Max (atms_of (D + negs (mset As)))"
using A_def As_def das by auto
then have "eligible As DA"
using eligible s_d_e As_def das maximal_wrt_def by auto
ultimately show ?thesis
using As_def by blast
next
assume s_d_e: "S DA ≠ {#}"
define As :: "'a list" where
"As = list_of_mset {#atm_of L. L ∈# S DA#}"
define D :: "'a clause" where
"D = DA - negs {#atm_of L. L ∈# S DA#}"
have "As ≠ []" unfolding As_def using s_d_e
by (metis image_mset_is_empty_iff list_of_mset_empty)
moreover have da_sub_as: "negs {#atm_of L. L ∈# S DA#} ⊆# DA"
using S_selects_subseteq by (auto simp: filter_neg_atm_of_S)
then have "negs (mset As) ⊆# DA"
unfolding As_def by auto
moreover have das: "DA = D + negs (mset As)"
using da_sub_as unfolding D_def As_def by auto
moreover have "S DA = negs {#atm_of L. L ∈# S DA#}"
by (auto simp: filter_neg_atm_of_S)
then have "S DA = negs (mset As)"
unfolding As_def by auto
then have "eligible As DA"
unfolding das using eligible by auto
ultimately show ?thesis
by blast
qed
then obtain As :: "'a list" where
as_ne: "As ≠ []" and
negs_as_le_d: "negs (mset As) ≤# DA" and
s_d: "eligible As DA"
by blast
define D :: "'a clause" where
"D = DA - negs (mset As)"
have "set As ⊆ INTERP N"
using d_cex negs_as_le_d by force
then have prod_ex: "∀A ∈ set As. ∃D. produces N D A"
unfolding INTERP_def
by (metis (no_types, lifting) INTERP_def subsetCE UN_E not_produces_imp_notin_production)
then have "⋀A. ∃D. produces N D A ⟶ A ∈ set As"
using ec_ni_n by (auto intro: productive_in_N)
then have "⋀A. ∃D. produces N D A ⟷ A ∈ set As"
using prod_ex by blast
then obtain CA_of where c_of0: "⋀A. produces N (CA_of A) A ⟷ A ∈ set As"
by metis
then have prod_c0: "∀A ∈ set As. produces N (CA_of A) A"
by blast
define C_of where
"⋀A. C_of A = {#L ∈# CA_of A. L ≠ Pos A#}"
define Aj_of where
"⋀A. Aj_of A = image_mset atm_of {#L ∈# CA_of A. L = Pos A#}"
have pospos: "⋀LL A. {#Pos (atm_of x). x ∈# {#L ∈# LL. L = Pos A#}#} = {#L ∈# LL. L = Pos A#}"
by (metis (mono_tags, lifting) image_filter_cong literal.sel(1) multiset.map_ident)
have ca_of_c_of_aj_of: "⋀A. CA_of A = C_of A + poss (Aj_of A)"
using pospos[of _ "CA_of _"] by (simp add: C_of_def Aj_of_def)
define n :: nat where
"n = length As"
define Cs :: "'a clause list" where
"Cs = map C_of As"
define AAs :: "'a multiset list" where
"AAs = map Aj_of As"
define CAs :: "'a literal multiset list" where
"CAs = map CA_of As"
have m_nz: "⋀A. A ∈ set As ⟹ Aj_of A ≠ {#}"
unfolding Aj_of_def using prod_c0 produces_imp_Pos_in_lits
by (metis (full_types) filter_mset_empty_conv image_mset_is_empty_iff)
have prod_c: "productive N CA" if ca_in: "CA ∈ set CAs" for CA
proof -
obtain i where i_p: "i < length CAs" "CAs ! i = CA"
using ca_in by (meson in_set_conv_nth)
have "production N (CA_of (As ! i)) = {As ! i}"
using i_p CAs_def prod_c0 by auto
then show "productive N CA"
using i_p CAs_def by auto
qed
then have cs_subs_n: "set CAs ⊆ N"
using productive_in_N by auto
have cs_true: "INTERP N ⊨m mset CAs"
unfolding true_cls_mset_def using prod_c productive_imp_INTERP by auto
have "⋀A. A ∈ set As ⟹ ¬ Neg A ∈# CA_of A"
using prod_c0 produces_imp_neg_notin_lits by auto
then have a_ni_c': "⋀A. A ∈ set As ⟹ A ∉ atms_of (C_of A)"
unfolding C_of_def using atm_imp_pos_or_neg_lit by force
have c'_le_c: "⋀A. C_of A ≤ CA_of A"
unfolding C_of_def by (auto intro: subset_eq_imp_le_multiset)
have a_max_c: "⋀A. A ∈ set As ⟹ A = Max (atms_of (CA_of A))"
using prod_c0 productive_imp_produces_Max_atom[of N] by auto
then have "⋀A. A ∈ set As ⟹ C_of A ≠ {#} ⟹ Max (atms_of (C_of A)) ≤ A"
using c'_le_c by (metis less_eq_Max_atms_of)
moreover have "⋀A. A ∈ set As ⟹ C_of A ≠ {#} ⟹ Max (atms_of (C_of A)) ≠ A"
using a_ni_c' Max_in by (metis (no_types) atms_empty_iff_empty finite_atms_of)
ultimately have max_c'_lt_a: "⋀A. A ∈ set As ⟹ C_of A ≠ {#} ⟹ Max (atms_of (C_of A)) < A"
by (metis order.strict_iff_order)
have le_cs_as: "length CAs = length As"
unfolding CAs_def by simp
have "length CAs = n"
by (simp add: le_cs_as n_def)
moreover have "length Cs = n"
by (simp add: Cs_def n_def)
moreover have "length AAs = n"
by (simp add: AAs_def n_def)
moreover have "length As = n"
using n_def by auto
moreover have "n ≠ 0"
by (simp add: as_ne n_def)
moreover have " ∀i. i < length AAs ⟶ (∀A ∈# AAs ! i. A = As ! i)"
using AAs_def Aj_of_def by auto
have "⋀x B. production N (CA_of x) = {x} ⟹ B ∈# CA_of x ⟹ B ≠ Pos x ⟹ atm_of B < x"
by (metis atm_of_lit_in_atms_of insert_not_empty le_imp_less_or_eq Pos_atm_of_iff
Neg_atm_of_iff pos_neg_in_imp_true produces_imp_Pos_in_lits produces_imp_atms_leq
productive_imp_not_interp)
then have "⋀B A. A∈set As ⟹ B ∈# CA_of A ⟹ B ≠ Pos A ⟹ atm_of B < A"
using prod_c0 by auto
have "∀i. i < length AAs ⟶ AAs ! i ≠ {#}"
unfolding AAs_def using m_nz by simp
have "∀i < n. CAs ! i = Cs ! i + poss (AAs ! i)"
unfolding CAs_def Cs_def AAs_def using ca_of_c_of_aj_of by (simp add: n_def)
moreover have "∀i < n. AAs ! i ≠ {#}"
using ‹∀i < length AAs. AAs ! i ≠ {#}› calculation(3) by blast
moreover have "∀i < n. ∀A ∈# AAs ! i. A = As ! i"
by (simp add: ‹∀i < length AAs. ∀A ∈# AAs ! i. A = As ! i› calculation(3))
moreover have "eligible As DA"
using s_d by auto
then have "eligible As (D + negs (mset As))"
using D_def negs_as_le_d by auto
moreover have "⋀i. i < length AAs ⟹ strictly_maximal_wrt (As ! i) ((Cs ! i))"
by (simp add: C_of_def Cs_def ‹⋀x B. ⟦production N (CA_of x) = {x}; B ∈# CA_of x; B ≠ Pos x⟧ ⟹ atm_of B < x› atms_of_def calculation(3) n_def prod_c0 strictly_maximal_wrt_def)
have "∀i < n. strictly_maximal_wrt (As ! i) (Cs ! i)"
by (simp add: ‹⋀i. i < length AAs ⟹ strictly_maximal_wrt (As ! i) (Cs ! i)› calculation(3))
moreover have "∀CA ∈ set CAs. S CA = {#}"
using prod_c producesD productive_imp_produces_Max_literal by blast
have "∀CA∈set CAs. S CA = {#}"
using ‹∀CA∈set CAs. S CA = {#}› by simp
then have "∀i < n. S (CAs ! i) = {#}"
using ‹length CAs = n› nth_mem by blast
ultimately have res_e: "ord_resolve CAs (D + negs (mset As)) AAs As (∑⇩# (mset Cs) + D)"
using ord_resolve by auto
have "⋀A. A ∈ set As ⟹ ¬ interp N (CA_of A) ⊨ CA_of A"
by (simp add: prod_c0 producesD)
then have "⋀A. A ∈ set As ⟹ ¬ Interp N (CA_of A) ⊨ C_of A"
unfolding prod_c0 C_of_def Interp_def true_cls_def using true_lit_def not_gr_zero prod_c0
by auto
then have c'_at_n: "⋀A. A ∈ set As ⟹ ¬ INTERP N ⊨ C_of A"
using a_max_c c'_le_c max_c'_lt_a not_Interp_imp_not_INTERP unfolding true_cls_def
by (metis true_cls_def true_cls_empty)
have "¬ INTERP N ⊨ ∑⇩# (mset Cs)"
unfolding Cs_def true_cls_def using c'_at_n by fastforce
moreover have "¬ INTERP N ⊨ D"
using d_cex by (metis D_def add_diff_cancel_right' negs_as_le_d subset_mset.add_diff_assoc2
true_cls_def union_iff)
ultimately have e_cex: "¬ INTERP N ⊨ ∑⇩# (mset Cs) + D"
by simp
have "set CAs ⊆ N"
by (simp add: cs_subs_n)
moreover have "INTERP N ⊨m mset CAs"
by (simp add: cs_true)
moreover have "⋀CA. CA ∈ set CAs ⟹ productive N CA"
by (simp add: prod_c)
moreover have "ord_resolve CAs DA AAs As (∑⇩# (mset Cs) + D)"
using D_def negs_as_le_d res_e by auto
moreover have "¬ INTERP N ⊨ ∑⇩# (mset Cs) + D"
using e_cex by simp
moreover have "∑⇩# (mset Cs) + D < DA"
using calculation(4) ord_resolve_reductive by auto
ultimately show thesis
..
qed
lemma ord_resolve_atms_of_concl_subset:
assumes "ord_resolve CAs DA AAs As E"
shows "atms_of E ⊆ (⋃C ∈ set CAs. atms_of C) ∪ atms_of DA"
using assms
proof (cases rule: ord_resolve.cases)
case (ord_resolve n Cs D)
note DA = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and cas = this(8)
have "∀i < n. set_mset (Cs ! i) ⊆ set_mset (CAs ! i)"
using cas by auto
then have "∀i < n. Cs ! i ⊆# ∑⇩# (mset CAs)"
by (metis cas cas_len mset_subset_eq_add_left nth_mem_mset sum_mset.remove union_assoc)
then have "∀C ∈ set Cs. C ⊆# ∑⇩# (mset CAs)"
using cs_len in_set_conv_nth[of _ Cs] by auto
then have "set_mset (∑⇩# (mset Cs)) ⊆ set_mset (∑⇩# (mset CAs))"
by auto (meson in_mset_sum_list2 mset_subset_eqD)
then have "atms_of (∑⇩# (mset Cs)) ⊆ atms_of (∑⇩# (mset CAs))"
by (meson lits_subseteq_imp_atms_subseteq mset_subset_eqD subsetI)
moreover have "atms_of (∑⇩# (mset CAs)) = (⋃CA ∈ set CAs. atms_of CA)"
by (intro set_eqI iffI, simp_all,
metis in_mset_sum_list2 atm_imp_pos_or_neg_lit neg_lit_in_atms_of pos_lit_in_atms_of,
metis in_mset_sum_list atm_imp_pos_or_neg_lit neg_lit_in_atms_of pos_lit_in_atms_of)
ultimately have "atms_of (∑⇩# (mset Cs)) ⊆ (⋃CA ∈ set CAs. atms_of CA)"
by auto
moreover have "atms_of D ⊆ atms_of DA"
using DA by auto
ultimately show ?thesis
unfolding e by auto
qed
subsection ‹Inference System›
text ‹
Theorem 3.16 is subsumed in the counterexample-reducing inference system framework, which is
instantiated below. Unlike its unordered cousin, ordered resolution is additionally a reductive
inference system.
›
definition ord_Γ :: "'a inference set" where
"ord_Γ = {Infer (mset CAs) DA E | CAs DA AAs As E. ord_resolve CAs DA AAs As E}"
sublocale ord_Γ_sound_counterex_reducing?:
sound_counterex_reducing_inference_system "ground_resolution_with_selection.ord_Γ S"
"ground_resolution_with_selection.INTERP S" +
reductive_inference_system "ground_resolution_with_selection.ord_Γ S"
proof unfold_locales
fix N :: "'a clause set" and DA :: "'a clause"
assume "{#} ∉ N" and "DA ∈ N" and "¬ INTERP N ⊨ DA" and "⋀C. C ∈ N ⟹ ¬ INTERP N ⊨ C ⟹ DA ≤ C"
then obtain CAs AAs As E where
dd_sset_n: "set CAs ⊆ N" and
dd_true: "INTERP N ⊨m mset CAs" and
res_e: "ord_resolve CAs DA AAs As E" and
e_cex: "¬ INTERP N ⊨ E" and
e_lt_c: "E < DA"
using ord_resolve_counterex_reducing[of N DA thesis] by auto
have "Infer (mset CAs) DA E ∈ ord_Γ"
using res_e unfolding ord_Γ_def by (metis (mono_tags, lifting) mem_Collect_eq)
then show "∃CC E. set_mset CC ⊆ N ∧ INTERP N ⊨m CC ∧ Infer CC DA E ∈ ord_Γ
∧ ¬ INTERP N ⊨ E ∧ E < DA"
using dd_sset_n dd_true e_cex e_lt_c by (metis set_mset_mset)
qed (auto simp: ord_Γ_def intro: ord_resolve_sound ord_resolve_reductive)
lemmas clausal_logic_compact = ord_Γ_sound_counterex_reducing.clausal_logic_compact
end
text ‹
A second proof of Theorem 3.12, compactness of clausal logic:
›
lemmas clausal_logic_compact = ground_resolution_with_selection.clausal_logic_compact
end