section ‹Refutational Inference Systems›
theory Inference_System
imports Herbrand_Interpretation
begin
text ‹
This theory gathers results from Section 2.4 (``Refutational Theorem Proving''), 3 (``Standard
Resolution''), and 4.2 (``Counterexample-Reducing Inference Systems'') of Bachmair and Ganzinger's
chapter.
›
subsection ‹Preliminaries›
text ‹
Inferences have one distinguished main premise, any number of side premises, and a conclusion.
›
datatype 'a inference =
Infer (side_prems_of: "'a clause multiset") (main_prem_of: "'a clause") (concl_of: "'a clause")
abbreviation prems_of :: "'a inference ⇒ 'a clause multiset" where
"prems_of γ ≡ side_prems_of γ + {#main_prem_of γ#}"
abbreviation concls_of :: "'a inference set ⇒ 'a clause set" where
"concls_of Γ ≡ concl_of ` Γ"
definition infer_from :: "'a clause set ⇒ 'a inference ⇒ bool" where
"infer_from CC γ ⟷ set_mset (prems_of γ) ⊆ CC"
locale inference_system =
fixes Γ :: "'a inference set"
begin
definition inferences_from :: "'a clause set ⇒ 'a inference set" where
"inferences_from CC = {γ. γ ∈ Γ ∧ infer_from CC γ}"
definition inferences_between :: "'a clause set ⇒ 'a clause ⇒ 'a inference set" where
"inferences_between CC C = {γ. γ ∈ Γ ∧ infer_from (CC ∪ {C}) γ ∧ C ∈# prems_of γ}"
lemma inferences_from_mono: "CC ⊆ DD ⟹ inferences_from CC ⊆ inferences_from DD"
unfolding inferences_from_def infer_from_def by fast
definition saturated :: "'a clause set ⇒ bool" where
"saturated N ⟷ concls_of (inferences_from N) ⊆ N"
lemma saturatedD:
assumes
satur: "saturated N" and
inf: "Infer CC D E ∈ Γ" and
cc_subs_n: "set_mset CC ⊆ N" and
d_in_n: "D ∈ N"
shows "E ∈ N"
proof -
have "Infer CC D E ∈ inferences_from N"
unfolding inferences_from_def infer_from_def using inf cc_subs_n d_in_n by simp
then have "E ∈ concls_of (inferences_from N)"
unfolding image_iff by (metis inference.sel(3))
then show "E ∈ N"
using satur unfolding saturated_def by blast
qed
end
text ‹
Satisfiability preservation is a weaker requirement than soundness.
›
locale sat_preserving_inference_system = inference_system +
assumes Γ_sat_preserving: "satisfiable N ⟹ satisfiable (N ∪ concls_of (inferences_from N))"
locale sound_inference_system = inference_system +
assumes Γ_sound: "Infer CC D E ∈ Γ ⟹ I ⊨m CC ⟹ I ⊨ D ⟹ I ⊨ E"
begin
lemma Γ_sat_preserving:
assumes sat_n: "satisfiable N"
shows "satisfiable (N ∪ concls_of (inferences_from N))"
proof -
obtain I where i: "I ⊨s N"
using sat_n by blast
then have "⋀CC D E. Infer CC D E ∈ Γ ⟹ set_mset CC ⊆ N ⟹ D ∈ N ⟹ I ⊨ E"
using Γ_sound unfolding true_clss_def true_cls_mset_def by (simp add: subset_eq)
then have "⋀γ. γ ∈ Γ ⟹ infer_from N γ ⟹ I ⊨ concl_of γ"
unfolding infer_from_def by (case_tac γ) clarsimp
then have "I ⊨s concls_of (inferences_from N)"
unfolding inferences_from_def image_def true_clss_def infer_from_def by blast
then have "I ⊨s N ∪ concls_of (inferences_from N)"
using i by simp
then show ?thesis
by blast
qed
sublocale sat_preserving_inference_system
by unfold_locales (erule Γ_sat_preserving)
end
locale reductive_inference_system = inference_system Γ for Γ :: "('a :: wellorder) inference set" +
assumes Γ_reductive: "γ ∈ Γ ⟹ concl_of γ < main_prem_of γ"
subsection ‹Refutational Completeness›
text ‹
Refutational completeness can be established once and for all for counterexample-reducing inference
systems. The material formalized here draws from both the general framework of Section 4.2 and the
concrete instances of Section 3.
›
locale counterex_reducing_inference_system =
inference_system Γ for Γ :: "('a :: wellorder) inference set" +
fixes I_of :: "'a clause set ⇒ 'a interp"
assumes Γ_counterex_reducing:
"{#} ∉ N ⟹ D ∈ N ⟹ ¬ I_of N ⊨ D ⟹ (⋀C. C ∈ N ⟹ ¬ I_of N ⊨ C ⟹ D ≤ C) ⟹
∃CC E. set_mset CC ⊆ N ∧ I_of N ⊨m CC ∧ Infer CC D E ∈ Γ ∧ ¬ I_of N ⊨ E ∧ E < D"
begin
lemma ex_min_counterex:
fixes N :: "('a :: wellorder) clause set"
assumes "¬ I ⊨s N"
shows "∃C ∈ N. ¬ I ⊨ C ∧ (∀D ∈ N. D < C ⟶ I ⊨ D)"
proof -
obtain C where "C ∈ N" and "¬ I ⊨ C"
using assms unfolding true_clss_def by auto
then have c_in: "C ∈ {C ∈ N. ¬ I ⊨ C}"
by blast
show ?thesis
using wf_eq_minimal[THEN iffD1, rule_format, OF wf_less_multiset c_in] by blast
qed
theorem saturated_model:
assumes
satur: "saturated N" and
ec_ni_n: "{#} ∉ N"
shows "I_of N ⊨s N"
proof -
have ec_ni_n: "{#} ∉ N"
using ec_ni_n by auto
{
assume "¬ I_of N ⊨s N"
then obtain D where
d_in_n: "D ∈ N" and
d_cex: "¬ I_of N ⊨ D" and
d_min: "⋀C. C ∈ N ⟹ C < D ⟹ I_of N ⊨ C"
by (meson ex_min_counterex)
then obtain CC E where
cc_subs_n: "set_mset CC ⊆ N" and
inf_e: "Infer CC D E ∈ Γ" and
e_cex: "¬ I_of N ⊨ E" and
e_lt_d: "E < D"
using Γ_counterex_reducing[OF ec_ni_n] not_less by metis
from cc_subs_n inf_e have "E ∈ N"
using d_in_n satur by (blast dest: saturatedD)
then have False
using e_cex e_lt_d d_min not_less by blast
}
then show ?thesis
by satx
qed
text ‹
Cf. Corollary 3.10:
›
corollary saturated_complete: "saturated N ⟹ ¬ satisfiable N ⟹ {#} ∈ N"
using saturated_model by blast
end
subsection ‹Compactness›
text ‹
Bachmair and Ganzinger claim that compactness follows from refutational completeness but leave the
proof to the readers' imagination. Our proof relies on an inductive definition of saturation in
terms of a base set of clauses.
›
context inference_system
begin
inductive_set saturate :: "'a clause set ⇒ 'a clause set" for CC :: "'a clause set" where
base: "C ∈ CC ⟹ C ∈ saturate CC"
| step: "Infer CC' D E ∈ Γ ⟹ (⋀C'. C' ∈# CC' ⟹ C' ∈ saturate CC) ⟹ D ∈ saturate CC ⟹
E ∈ saturate CC"
lemma saturate_mono: "C ∈ saturate CC ⟹ CC ⊆ DD ⟹ C ∈ saturate DD"
by (induct rule: saturate.induct) (auto intro: saturate.intros)
lemma saturated_saturate[simp, intro]: "saturated (saturate N)"
unfolding saturated_def inferences_from_def infer_from_def image_def
by clarify (rename_tac x, case_tac x, auto elim!: saturate.step)
lemma saturate_finite: "C ∈ saturate CC ⟹ ∃DD. DD ⊆ CC ∧ finite DD ∧ C ∈ saturate DD"
proof (induct rule: saturate.induct)
case (base C)
then have "{C} ⊆ CC" and "finite {C}" and "C ∈ saturate {C}"
by (auto intro: saturate.intros)
then show ?case
by blast
next
case (step CC' D E)
obtain DD_of where
"⋀C. C ∈# CC' ⟹ DD_of C ⊆ CC ∧ finite (DD_of C) ∧ C ∈ saturate (DD_of C)"
using step(3) by metis
then have
"(⋃C ∈ set_mset CC'. DD_of C) ⊆ CC"
"finite (⋃C ∈ set_mset CC'. DD_of C) ∧ set_mset CC' ⊆ saturate (⋃C ∈ set_mset CC'. DD_of C)"
by (auto intro: saturate_mono)
then obtain DD where
d_sub: "DD ⊆ CC" and d_fin: "finite DD" and in_sat_d: "set_mset CC' ⊆ saturate DD"
by blast
obtain EE where
e_sub: "EE ⊆ CC" and e_fin: "finite EE" and in_sat_ee: "D ∈ saturate EE"
using step(5) by blast
have "DD ∪ EE ⊆ CC"
using d_sub e_sub step(1) by fast
moreover have "finite (DD ∪ EE)"
using d_fin e_fin by fast
moreover have "E ∈ saturate (DD ∪ EE)"
using in_sat_d in_sat_ee step.hyps(1)
by (blast intro: inference_system.saturate.step saturate_mono)
ultimately show ?case
by blast
qed
end
context sound_inference_system
begin
theorem saturate_sound: "C ∈ saturate CC ⟹ I ⊨s CC ⟹ I ⊨ C"
by (induct rule: saturate.induct) (auto simp: true_cls_mset_def true_clss_def Γ_sound)
end
context sat_preserving_inference_system
begin
text ‹
This result surely holds, but we have yet to prove it. The challenge is: Every time a new clause is
introduced, we also get a new interpretation (by the definition of
‹sat_preserving_inference_system›). But the interpretation we want here is then the one that
exists "at the limit". Maybe we can use compactness to prove it.
›
theorem saturate_sat_preserving: "satisfiable CC ⟹ satisfiable (saturate CC)"
oops
end
locale sound_counterex_reducing_inference_system =
counterex_reducing_inference_system + sound_inference_system
begin
text ‹
Compactness of clausal logic is stated as Theorem 3.12 for the case of unordered ground resolution.
The proof below is a generalization to any sound counterexample-reducing inference system. The
actual theorem will become available once the locale has been instantiated with a concrete inference
system.
›
theorem clausal_logic_compact:
fixes N :: "('a :: wellorder) clause set"
shows "¬ satisfiable N ⟷ (∃DD ⊆ N. finite DD ∧ ¬ satisfiable DD)"
proof
assume "¬ satisfiable N"
then have "{#} ∈ saturate N"
using saturated_complete saturated_saturate saturate.base unfolding true_clss_def by meson
then have "∃DD ⊆ N. finite DD ∧ {#} ∈ saturate DD"
using saturate_finite by fastforce
then show "∃DD ⊆ N. finite DD ∧ ¬ satisfiable DD"
using saturate_sound by auto
next
assume "∃DD ⊆ N. finite DD ∧ ¬ satisfiable DD"
then show "¬ satisfiable N"
by (blast intro: true_clss_mono)
qed
end
end