Theory Ordered_Resolution_Prover.Unordered_Ground_Resolution
section ‹Ground Unordered Resolution Calculus›
theory Unordered_Ground_Resolution
imports Inference_System Ground_Resolution_Model
begin
text ‹
Unordered ground resolution is one of the two inference systems studied in Section 3 (``Standard
Resolution'') of Bachmair and Ganzinger's chapter.
›
subsection ‹Inference Rule›
text ‹
Unordered ground resolution consists of a single rule, called ‹unord_resolve› below, which is
sound and counterexample-reducing.
›
locale ground_resolution_without_selection
begin
sublocale ground_resolution_with_selection where S = "λ_. {#}"
by unfold_locales auto
inductive unord_resolve :: "'a clause ⇒ 'a clause ⇒ 'a clause ⇒ bool" where
"unord_resolve (C + replicate_mset (Suc n) (Pos A)) (add_mset (Neg A) D) (C + D)"
lemma unord_resolve_sound: "unord_resolve C D E ⟹ I ⊨ C ⟹ I ⊨ D ⟹ I ⊨ E"
using unord_resolve.cases by fastforce
text ‹
The following result corresponds to Theorem 3.8, except that the conclusion is strengthened slightly
to make it fit better with the counterexample-reducing inference system framework.
›
theorem unord_resolve_counterex_reducing:
assumes
ec_ni_n: "{#} ∉ N" and
c_in_n: "C ∈ N" and
c_cex: "¬ INTERP N ⊨ C" and
c_min: "⋀D. D ∈ N ⟹ ¬ INTERP N ⊨ D ⟹ C ≤ D"
obtains D E where
"D ∈ N"
"INTERP N ⊨ D"
"productive N D"
"unord_resolve D C E"
"¬ INTERP N ⊨ E"
"E < C"
proof -
have c_ne: "C ≠ {#}"
using c_in_n ec_ni_n by blast
have "∃A. A ∈ atms_of C ∧ A = Max (atms_of C)"
using c_ne by (blast intro: Max_in_lits atm_of_Max_lit atm_of_lit_in_atms_of)
then have "∃A. Neg A ∈# C"
using c_ne c_in_n c_cex c_min Max_in_lits Max_lit_eq_pos_or_neg_Max_atm max_pos_imp_Interp
Interp_imp_INTERP by metis
then obtain A where neg_a_in_c: "Neg A ∈# C"
by blast
then obtain C' where c: "C = add_mset (Neg A) C'"
using insert_DiffM by metis
have "A ∈ INTERP N"
using neg_a_in_c c_cex[unfolded true_cls_def] by fast
then obtain D where d0: "produces N D A"
unfolding INTERP_def by (metis UN_E not_produces_imp_notin_production)
have prod_d: "productive N D"
unfolding d0 by simp
then have d_in_n: "D ∈ N"
using productive_in_N by fast
have d_true: "INTERP N ⊨ D"
using prod_d productive_imp_INTERP by blast
obtain D' AAA where
d: "D = D' + AAA" and
d': "D' = {#L ∈# D. L ≠ Pos A#}" and
aa: "AAA = {#L ∈# D. L = Pos A#}"
using multiset_partition union_commute by metis
have d'_subs: "set_mset D' ⊆ set_mset D"
unfolding d' by auto
have "¬ Neg A ∈# D"
using d0 by (blast dest: produces_imp_neg_notin_lits)
then have neg_a_ni_d': "¬ Neg A ∈# D'"
using d'_subs by auto
have a_ni_d': "A ∉ atms_of D'"
using d' neg_a_ni_d' by (auto dest: atm_imp_pos_or_neg_lit)
have "∃n. AAA = replicate_mset (Suc n) (Pos A)"
using aa d0 not0_implies_Suc produces_imp_Pos_in_lits[of N]
by (simp add: filter_eq_replicate_mset del: replicate_mset_Suc)
then have res_e: "unord_resolve D C (D' + C')"
unfolding c d by (fastforce intro: unord_resolve.intros)
have d'_le_d: "D' ≤ D"
unfolding d by simp
have a_max_d: "A = Max (atms_of D)"
using d0 productive_imp_produces_Max_atom by auto
then have "D' ≠ {#} ⟹ Max (atms_of D') ≤ A"
using d'_le_d by (blast intro: less_eq_Max_atms_of)
moreover have "D' ≠ {#} ⟹ Max (atms_of D') ≠ A"
using a_ni_d' Max_in by (blast intro: atms_empty_iff_empty[THEN iffD1])
ultimately have max_d'_lt_a: "D' ≠ {#} ⟹ Max (atms_of D') < A"
using dual_order.strict_iff_order by blast
have "¬ interp N D ⊨ D"
using d0 productive_imp_not_interp by blast
then have "¬ Interp N D ⊨ D'"
unfolding d0 d' Interp_def true_cls_def by (auto simp: true_lit_def simp del: not_gr_zero)
then have "¬ INTERP N ⊨ D'"
using a_max_d d'_le_d max_d'_lt_a not_Interp_imp_not_INTERP by blast
moreover have "¬ INTERP N ⊨ C'"
using c_cex unfolding c by simp
ultimately have e_cex: "¬ INTERP N ⊨ D' + C'"
by simp
have "⋀B. B ∈ atms_of D' ⟹ B ≤ A"
using d0 d'_subs contra_subsetD lits_subseteq_imp_atms_subseteq produces_imp_atms_leq by metis
then have "⋀L. L ∈# D' ⟹ L < Neg A"
using neg_a_ni_d' antisym_conv1 atms_less_eq_imp_lit_less_eq_neg by metis
then have lt_cex: "D' + C' < C"
by (force intro: add.commute simp: c less_multiset⇩D⇩M intro: exI[of _ "{#Neg A#}"])
from d_in_n d_true prod_d res_e e_cex lt_cex show ?thesis ..
qed
subsection ‹Inference System›
text ‹
Theorem 3.9 and Corollary 3.10 are subsumed in the counterexample-reducing inference system
framework, which is instantiated below.
›
definition unord_Γ :: "'a inference set" where
"unord_Γ = {Infer {#C#} D E | C D E. unord_resolve C D E}"
sublocale unord_Γ_sound_counterex_reducing?:
sound_counterex_reducing_inference_system unord_Γ INTERP
proof unfold_locales
fix D E and N :: "('b :: wellorder) clause set"
assume "{#} ∉ N" and "D ∈ N" and "¬ INTERP N ⊨ D" and "⋀C. C ∈ N ⟹ ¬ INTERP N ⊨ C ⟹ D ≤ C"
then obtain C E where
c_in_n: "C ∈ N" and
c_true: "INTERP N ⊨ C" and
res_e: "unord_resolve C D E" and
e_cex: "¬ INTERP N ⊨ E" and
e_lt_d: "E < D"
using unord_resolve_counterex_reducing by (metis (no_types))
from c_in_n have "set_mset {#C#} ⊆ N"
by auto
moreover have "Infer {#C#} D E ∈ unord_Γ"
unfolding unord_Γ_def using res_e by blast
ultimately show
"∃CC E. set_mset CC ⊆ N ∧ INTERP N ⊨m CC ∧ Infer CC D E ∈ unord_Γ ∧ ¬ INTERP N ⊨ E ∧ E < D"
using c_in_n c_true e_cex e_lt_d by blast
next
fix CC D E and I :: "'b interp"
assume "Infer CC D E ∈ unord_Γ" and "I ⊨m CC" and "I ⊨ D"
then show "I ⊨ E"
by (clarsimp simp: unord_Γ_def true_cls_mset_def) (erule unord_resolve_sound, auto)
qed
lemmas clausal_logic_compact = unord_Γ_sound_counterex_reducing.clausal_logic_compact
end
text ‹
Theorem 3.12, compactness of clausal logic, has finally been derived for a concrete inference
system:
›
lemmas clausal_logic_compact = ground_resolution_without_selection.clausal_logic_compact
end