Theory Prime_Implicates
section ‹Prime Implicates Generation›
text ‹We show that the unrestricted resolution rule is deductive complete, i.e. that it is able
to generate all (prime) implicates of any given clause set.›
theory Prime_Implicates
imports Propositional_Resolution
begin
context propositional_atoms
begin
subsection ‹Implicates and Prime Implicates›
text ‹We first introduce the definitions of implicates and prime implicates.›
definition implicates :: "'at Formula ⇒ 'at Formula"
where "implicates S = { C. entails S C }"
definition prime_implicates :: "'at Formula ⇒ 'at Formula"
where "prime_implicates S = simplify (implicates S)"
subsection ‹Generation of Prime Implicates›
text ‹We introduce a function simplifying a given clause set by evaluating some literals
to false. We show that this partial evaluation operation preserves saturatedness and
that if the considered set of literals is an implicate of the initial clause set
then the partial evaluation yields a clause set that is unsatisfiable.
Then the proof follows from refutational completeness: since the partially evaluated set
is unsatisfiable and saturated it must contain the empty clause, and therefore the initial
clause set necessarily contains a clause subsuming the implicate.›
fun partial_evaluation :: "'a Formula ⇒ 'a Literal set ⇒ 'a Formula"
where
"(partial_evaluation S C) = { E. ∃D. D ∈ S ∧ E = D-C ∧ ¬(∃L. (L ∈ C) ∧ (complement L) ∈ D)}"
lemma partial_evaluation_is_saturated :
assumes "saturated_binary_rule resolvent S"
shows "saturated_binary_rule ordered_resolvent (partial_evaluation S C)"
proof (rule ccontr)
let ?peval = "partial_evaluation S C"
assume "¬saturated_binary_rule ordered_resolvent ?peval"
from this obtain P1 and P2 and R where "P1 ∈ ?peval" and "P2 ∈ ?peval"
and "ordered_resolvent P1 P2 R" and "¬(tautology R)"
and not_subsumed: "¬(∃D. ((D ∈ (partial_evaluation S C)) ∧ (subsumes D R)))"
unfolding saturated_binary_rule_def and redundant_def by auto
from ‹P1 ∈ ?peval› obtain PP1 where "PP1 ∈ S" and "P1 = PP1 - C"
and i: "¬(∃L. (L ∈ C) ∧ (complement L) ∈ PP1)" by auto
from ‹P2 ∈ ?peval› obtain PP2 where "PP2 ∈ S" and "P2 = PP2 - C"
and ii: "¬(∃L. (L ∈ C) ∧ (complement L) ∈ PP2)" by auto
from ‹(ordered_resolvent P1 P2 R)› obtain A where
r_def: "R = (P1 - { Pos A }) ∪ (P2 - { Neg A })" and "(Pos A) ∈ P1" and "(Neg A) ∈ P2"
unfolding ordered_resolvent_def strictly_maximal_literal_def by auto
let ?RR = "(PP1 - { Pos A }) ∪ (PP2 - { Neg A })"
from ‹P1 = PP1 - C› and ‹(Pos A) ∈ P1› have "(Pos A) ∈ PP1" by auto
from ‹P2 = PP2 - C› and ‹(Neg A) ∈ P2› have "(Neg A) ∈ PP2" by auto
from r_def and ‹P1 = PP1 - C› and ‹P2 = PP2 - C› have "R = ?RR - C" by auto
from ‹(Pos A) ∈ PP1› and ‹(Neg A) ∈ PP2›
have "resolvent PP1 PP2 ?RR" unfolding resolvent_def by auto
with ‹PP1 ∈ S› and ‹PP2 ∈ S› and ‹saturated_binary_rule resolvent S›
have "tautology ?RR ∨ (∃D. (D ∈ S ∧ (subsumes D ?RR)))"
unfolding saturated_binary_rule_def redundant_def by auto
thus "False"
proof
assume "tautology ?RR"
with ‹R = ?RR - C› and ‹¬tautology R›
obtain X where "X ∈ C" and "complement X ∈ PP1 ∪ PP2"
unfolding tautology_def by auto
from ‹X ∈ C› and ‹complement X ∈ PP1 ∪ PP2› and i and ii
show "False" by auto
next
assume "∃D. ((D ∈ S) ∧ (subsumes D ?RR))"
from this obtain D where "D ∈ S" and "subsumes D ?RR"
by auto
from ‹subsumes D ?RR› and ‹R = ?RR - C›
have "subsumes (D - C) R" unfolding subsumes_def by auto
from ‹D ∈ S› and ii and i and ‹(subsumes D ?RR)› have "D - C ∈ ?peval"
unfolding subsumes_def by auto
with ‹subsumes (D - C) R› and not_subsumed show "False" by auto
qed
qed
lemma evaluation_wrt_implicate_is_unsat :
assumes "entails S C"
assumes "¬tautology C"
shows "¬satisfiable (partial_evaluation S C)"
proof
let ?peval = "partial_evaluation S C"
assume "satisfiable ?peval"
then obtain I where "validate_formula I ?peval" unfolding satisfiable_def by auto
let ?J = "(I - { X. (Pos X) ∈ C }) ∪ { Y. (Neg Y) ∈ C }"
have "¬validate_clause ?J C"
proof
assume "validate_clause ?J C"
then obtain L where "L ∈ C" and "validate_literal ?J L" by auto
obtain X where "L = (Pos X) ∨ L = (Neg X)" using Literal.exhaust [of L] by auto
from ‹L = (Pos X) ∨ L = (Neg X)› and ‹L ∈ C› and ‹¬tautology C› and ‹validate_literal ?J L›
show "False" unfolding tautology_def by auto
qed
have "validate_formula ?J S"
proof (rule ccontr)
assume "¬ (validate_formula ?J S)"
then obtain D where "D ∈ S" and "¬(validate_clause ?J D)" by auto
from ‹D ∈ S› have "D-C ∈ ?peval ∨ (∃L. (L ∈ C) ∧ (complement L) ∈ D)"
by auto
thus "False"
proof
assume "∃L. (L ∈ C) ∧ (complement L) ∈ D"
then obtain L where "L ∈ C" and "complement L ∈ D" by auto
obtain X where "L = (Pos X) ∨ L = (Neg X)" using Literal.exhaust [of L] by auto
from this and ‹L ∈ C› and ‹¬(tautology C)› have "validate_literal ?J (complement L)"
unfolding tautology_def by auto
from ‹(validate_literal ?J (complement L))› and ‹(complement L) ∈ D›
and ‹¬(validate_clause ?J D)›
show "False" by auto
next
assume "D-C ∈ ?peval"
from ‹D-C ∈ ?peval› and ‹(validate_formula I ?peval)›
have "validate_clause I (D-C)" using validate_formula.simps by blast
from this obtain L where "L ∈ D" and "L ∉ C" and "validate_literal I L" by auto
obtain X where "L = (Pos X) ∨ L = (Neg X)" using Literal.exhaust [of L] by auto
from ‹L = (Pos X) ∨ L = (Neg X)› and ‹validate_literal I L› and ‹L ∉ C›
have "validate_literal ?J L" unfolding tautology_def by auto
from ‹validate_literal ?J L› and ‹L ∈ D› and ‹¬(validate_clause ?J D)›
show "False" by auto
qed
qed
from ‹¬validate_clause ?J C› and ‹validate_formula ?J S› and ‹entails S C› show "False"
unfolding entails_def by auto
qed
lemma entailment_and_implicates:
assumes "entails_formula S1 S2"
shows "implicates S2 ⊆ implicates S1"
using assms entailed_formula_entails_implicates implicates_def by auto
lemma equivalence_and_implicates:
assumes "equivalent S1 S2"
shows "implicates S1 = implicates S2"
using assms entailment_and_implicates equivalent_def by blast
lemma equivalence_and_prime_implicates:
assumes "equivalent S1 S2"
shows "prime_implicates S1 = prime_implicates S2"
using assms equivalence_and_implicates prime_implicates_def by auto
lemma unrestricted_resolution_is_deductive_complete :
assumes "saturated_binary_rule resolvent S"
assumes "all_fulfill finite S"
assumes "C ∈ implicates S"
shows "redundant C S"
proof ((cases "tautology C"),(simp add: redundant_def))
next
assume "¬ tautology C"
have "∃D. (D ∈ S) ∧ (subsumes D C)"
proof -
let ?peval = "partial_evaluation S C"
from ‹saturated_binary_rule resolvent S›
have "saturated_binary_rule ordered_resolvent ?peval"
using partial_evaluation_is_saturated by auto
from ‹C ∈ implicates S› have "entails S C" unfolding implicates_def by auto
from ‹entails S C› and ‹¬tautology C› have "¬satisfiable ?peval"
using evaluation_wrt_implicate_is_unsat by auto
from ‹all_fulfill finite S› have "all_fulfill finite ?peval" unfolding all_fulfill_def by auto
from ‹¬satisfiable ?peval› and ‹saturated_binary_rule ordered_resolvent ?peval›
and ‹all_fulfill finite ?peval›
have "{} ∈ ?peval" using Complete_def ordered_resolution_is_complete by blast
then show ?thesis unfolding subsumes_def by auto
qed
then show ?thesis unfolding redundant_def by auto
qed
lemma prime_implicates_generation_correct :
assumes "saturated_binary_rule resolvent S"
assumes "non_redundant S"
assumes "all_fulfill finite S"
shows "S ⊆ prime_implicates S"
proof
fix x assume "x ∈ S"
show "x ∈ prime_implicates S"
proof (rule ccontr)
assume "¬ x ∈ prime_implicates S"
from ‹x ∈ S› have "entails S x" unfolding entails_def implicates_def by auto
then have "x ∈ implicates S" unfolding implicates_def by auto
with ‹¬ x ∈ (prime_implicates S)› have "strictly_redundant x (implicates S)"
unfolding prime_implicates_def simplify_def by auto
from this have "tautology x ∨ (∃y. (y ∈ (implicates S)) ∧ (y ⊂ x))"
unfolding strictly_redundant_def by auto
then have "strictly_redundant x S"
proof ((cases "tautology x"),(simp add: strictly_redundant_def))
next
assume "¬tautology x"
with ‹tautology x ∨ (∃y. (y ∈ (implicates S)) ∧ (y ⊂ x))›
obtain y where "y ∈ implicates S" and "y ⊂ x" by auto
from ‹y ∈ implicates S› and ‹saturated_binary_rule resolvent S› and ‹all_fulfill finite S›
have "redundant y S" using unrestricted_resolution_is_deductive_complete by auto
from ‹y ⊂ x› and ‹¬tautology x› have "¬tautology y" unfolding tautology_def by auto
with ‹redundant y S› obtain z where "z ∈ S" and "z ⊆ y"
unfolding redundant_def subsumes_def by auto
with ‹y ⊂ x› have "z ⊂ x" by auto
with ‹z ∈ S› show "strictly_redundant x S" using strictly_redundant_def by auto
qed
with ‹non_redundant S› and ‹x ∈ S› show "False" unfolding non_redundant_def by auto
qed
qed
theorem prime_implicates_of_saturated_sets:
assumes "saturated_binary_rule resolvent S"
assumes "all_fulfill finite S"
assumes "non_redundant S"
shows "S = prime_implicates S"
proof
from assms show "S ⊆ prime_implicates S" using prime_implicates_generation_correct by auto
show "prime_implicates S ⊆ S"
proof
fix x assume "x ∈ prime_implicates S"
from this have "x ∈ implicates S" unfolding prime_implicates_def simplify_def by auto
with assms have "redundant x S"
using unrestricted_resolution_is_deductive_complete by auto
show "x ∈ S"
proof (rule ccontr)
assume "x ∉ S"
with ‹redundant x S› have "strictly_redundant x S"
unfolding redundant_def strictly_redundant_def subsumes_def by auto
with ‹S ⊆ prime_implicates S› have "strictly_redundant x (prime_implicates S)"
unfolding strictly_redundant_def by auto
then have "strictly_redundant x (implicates S)"
unfolding strictly_redundant_def prime_implicates_def simplify_def by auto
with ‹x ∈ prime_implicates S› show "False"
unfolding prime_implicates_def simplify_def by auto
qed
qed
qed
subsection ‹Incremental Prime Implicates Computation›
text ‹We show that it is possible to compute the set of prime implicates incrementally
i.e., to fix an ordering among atoms, and to compute the set of resolvents upon each atom
one by one, without backtracking (in the sense that if the resolvents upon a given atom are
generated at some step @{ term i } then no resolvents upon the same atom are generated at
step @{ term "j>i" }.
This feature is critical in practice for the efficiency of prime implicates
generation algorithms.›
text ‹We first introduce a function computing all resolvents upon a given atom.›
definition all_resolvents_upon :: "'at Formula ⇒ 'at ⇒ 'at Formula"
where "(all_resolvents_upon S A) = { C. ∃P1 P2. P1 ∈ S ∧ P2 ∈ S ∧ C = (resolvent_upon P1 P2 A) }"
lemma resolvent_upon_correct:
assumes "P1 ∈ S"
assumes "P2 ∈ S"
assumes "C = resolvent_upon P1 P2 A"
shows "entails S C"
proof cases
assume "Pos A ∈ P1 ∧ Neg A ∈ P2"
with ‹C = resolvent_upon P1 P2 A› have "resolvent P1 P2 C"
unfolding resolvent_def by auto
with ‹P1 ∈ S› and ‹P2 ∈ S› show ?thesis
using soundness_and_entailment resolution_is_correct by auto
next
assume "¬ (Pos A ∈ P1 ∧ Neg A ∈ P2)"
with ‹C = resolvent_upon P1 P2 A› have "P1 ⊆ C ∨ P2 ⊆ C" by auto
with ‹P1 ∈ S› and ‹P2 ∈ S› have "redundant C S"
unfolding redundant_def subsumes_def by auto
then show ?thesis using redundancy_implies_entailment by auto
qed
lemma all_resolvents_upon_is_finite:
assumes "all_fulfill finite S"
shows "all_fulfill finite (S ∪ (all_resolvents_upon S A))"
using assms unfolding all_fulfill_def all_resolvents_upon_def by auto
lemma atoms_formula_resolvents:
shows "atoms_formula (all_resolvents_upon S A) ⊆ atoms_formula S"
unfolding all_resolvents_upon_def by auto
text ‹We define a partial saturation predicate that is restricted to a specific atom.›
definition partial_saturation :: "'at Formula ⇒ 'at ⇒ 'at Formula ⇒ bool"
where
"(partial_saturation S A R) = (∀P1 P2. (P1 ∈ S ⟶ P2 ∈ S
⟶(redundant (resolvent_upon P1 P2 A) R)))"
text ‹We show that the resolvent of two redundant clauses in a partially saturated set
is itself redundant.›
lemma resolvent_upon_and_partial_saturation :
assumes "redundant P1 S"
assumes "redundant P2 S"
assumes "partial_saturation S A (S ∪ R)"
assumes "C = resolvent_upon P1 P2 A"
shows "redundant C (S ∪ R)"
proof (rule ccontr)
assume "¬redundant C (S ∪ R)"
from ‹C = resolvent_upon P1 P2 A› have "C = (P1 - { Pos A }) ∪ (P2 - { Neg A })" by auto
from ‹¬redundant C (S ∪ R)› have "¬tautology C" unfolding redundant_def by auto
have "¬ (tautology P1)"
proof
assume "tautology P1"
then obtain B where "Pos B ∈ P1" and "Neg B ∈ P1" unfolding tautology_def by auto
show "False"
proof cases
assume "A = B"
with ‹Neg B ∈ P1› and ‹C = (P1 - { Pos A }) ∪ (P2 - { Neg A })› have "subsumes P2 C"
unfolding subsumes_def using Literal.distinct by blast
with ‹redundant P2 S› have "redundant C S"
using subsumption_preserves_redundancy by auto
with ‹¬redundant C (S ∪ R)› show "False" unfolding redundant_def by auto
next
assume "A ≠ B"
with ‹C = (P1 - { Pos A }) ∪ (P2 - { Neg A })› and ‹Pos B ∈ P1› and ‹Neg B ∈ P1›
have "Pos B ∈ C" and "Neg B ∈ C" by auto
with ‹¬redundant C (S ∪ R)› show "False"
unfolding tautology_def redundant_def by auto
qed
qed
with ‹redundant P1 S› obtain Q1 where "Q1 ∈ S" and "subsumes Q1 P1"
unfolding redundant_def by auto
have "¬ (tautology P2)"
proof
assume "tautology P2"
then obtain B where "Pos B ∈ P2" and "Neg B ∈ P2" unfolding tautology_def by auto
show "False"
proof cases
assume "A = B"
with ‹Pos B ∈ P2› and ‹C = (P1 - { Pos A }) ∪ (P2 - { Neg A })› have "subsumes P1 C"
unfolding subsumes_def using Literal.distinct by blast
with ‹redundant P1 S› have "redundant C S"
using subsumption_preserves_redundancy by auto
with ‹¬redundant C (S ∪ R)› show "False" unfolding redundant_def by auto
next
assume "A ≠ B"
with ‹C = (P1 - { Pos A }) ∪ (P2 - { Neg A })› and ‹Pos B ∈ P2› and ‹Neg B ∈ P2›
have "Pos B ∈ C" and "Neg B ∈ C" by auto
with ‹¬redundant C (S ∪ R)› show "False"
unfolding tautology_def redundant_def by auto
qed
qed
with ‹redundant P2 S› obtain Q2 where "Q2 ∈ S" and "subsumes Q2 P2"
unfolding redundant_def by auto
let ?res = "(Q1 - { Pos A }) ∪ (Q2 - { Neg A })"
have "?res = resolvent_upon Q1 Q2 A" by auto
from this and ‹partial_saturation S A (S ∪ R)› and ‹Q1 ∈ S› and ‹Q2 ∈ S›
have "redundant ?res (S ∪ R)"
unfolding partial_saturation_def by auto
from ‹subsumes Q1 P1› and ‹subsumes Q2 P2› and ‹C = (P1 - { Pos A }) ∪ (P2 - { Neg A })›
have "subsumes ?res C" unfolding subsumes_def by auto
with ‹redundant ?res (S ∪ R)› and ‹¬redundant C (S ∪ R)› show False
using subsumption_preserves_redundancy by auto
qed
text ‹We show that if @{term R} is a set of resolvents of a set of clauses @{term S} then the
same holds for @{ term "S ∪ R"}. For the clauses in @{term S}, the premises are identical to
the resolvent and the inference is thus redundant (this trick is useful to simplify proofs).›
definition in_all_resolvents_upon:: "'at Formula ⇒ 'at ⇒ 'at Clause ⇒ bool"
where
"in_all_resolvents_upon S A C = (∃ P1 P2. (P1 ∈ S ∧ P2 ∈ S ∧ C = resolvent_upon P1 P2 A))"
lemma every_clause_is_a_resolvent:
assumes "all_fulfill (in_all_resolvents_upon S A) R"
assumes "all_fulfill (λx. ¬(tautology x)) S"
assumes "P1 ∈ S ∪ R"
shows "in_all_resolvents_upon S A P1"
proof ((cases "P1 ∈ R"),(metis all_fulfill_def assms(1)))
next
assume "P1 ∉ R"
with ‹P1 ∈ S ∪ R› have "P1 ∈ S" by auto
with ‹(all_fulfill (λx. ¬(tautology x)) S )› have "¬ tautology P1"
unfolding all_fulfill_def by auto
from ‹¬ tautology P1› have "Neg A ∉ P1 ∨ Pos A ∉ P1" unfolding tautology_def by auto
from this have "P1 = (P1 - { Pos A }) ∪ (P1 - { Neg A })" by auto
with ‹P1 ∈ S› show ?thesis unfolding resolvent_def
unfolding in_all_resolvents_upon_def by auto
qed
text ‹We show that if a formula is partially saturated then it stays so when new resolvents
are added in the set.›
lemma partial_saturation_is_preserved :
assumes "partial_saturation S E1 S"
assumes "partial_saturation S E2 (S ∪ R)"
assumes "all_fulfill (λx. ¬(tautology x)) S"
assumes "all_fulfill (in_all_resolvents_upon S E2) R"
shows "partial_saturation (S ∪ R) E1 (S ∪ R)"
proof (rule ccontr)
assume "¬ partial_saturation (S ∪ R) E1 (S ∪ R)"
from this obtain P1 P2 C where "P1 ∈ S ∪ R" and "P2 ∈ S ∪ R" and "C = resolvent_upon P1 P2 E1"
and "¬ redundant C (S ∪ R)"
unfolding partial_saturation_def by auto
from ‹C = resolvent_upon P1 P2 E1› have "C = (P1 - { Pos E1 }) ∪ (P2 - { Neg E1 })" by auto
from ‹P1 ∈ S ∪ R› and assms(4) and ‹(all_fulfill (λx. ¬(tautology x)) S )›
have "in_all_resolvents_upon S E2 P1" using every_clause_is_a_resolvent by auto
then obtain P1_1 P1_2 where "P1_1 ∈ S" and "P1_2 ∈ S" and "P1 = resolvent_upon P1_1 P1_2 E2"
using every_clause_is_a_resolvent unfolding in_all_resolvents_upon_def by blast
from ‹P2 ∈ S ∪ R› and assms(4) and ‹(all_fulfill (λx. ¬(tautology x)) S )›
have "in_all_resolvents_upon S E2 P2" using every_clause_is_a_resolvent by auto
then obtain P2_1 P2_2 where "P2_1 ∈ S" and "P2_2 ∈ S" and "P2 = resolvent_upon P2_1 P2_2 E2"
using every_clause_is_a_resolvent unfolding in_all_resolvents_upon_def by blast
let ?R1 = "resolvent_upon P1_1 P2_1 E1"
from ‹partial_saturation S E1 S› and ‹P1_1 ∈ S› and ‹P2_1 ∈ S› have "redundant ?R1 S"
unfolding partial_saturation_def by auto
let ?R2 = "resolvent_upon P1_2 P2_2 E1"
from ‹partial_saturation S E1 S› and ‹P1_2 ∈ S› and ‹P2_2 ∈ S› have "redundant ?R2 S"
unfolding partial_saturation_def by auto
let ?C = "resolvent_upon ?R1 ?R2 E2"
from ‹C = resolvent_upon P1 P2 E1› and ‹P2 = resolvent_upon P2_1 P2_2 E2›
and ‹P1 = resolvent_upon P1_1 P1_2 E2›
have "?C = C" by auto
with ‹redundant ?R1 S› and ‹redundant ?R2 S› and ‹partial_saturation S E2 (S ∪ R)›
and ‹¬ redundant C (S ∪ R)›
show "False" using resolvent_upon_and_partial_saturation by auto
qed
text ‹The next lemma shows that the clauses inferred by applying the resolution rule
upon a given atom contain no occurrence of this atom, unless the inference is redundant.›
lemma resolvents_do_not_contain_atom :
assumes "¬ tautology P1"
assumes "¬ tautology P2"
assumes "C = resolvent_upon P1 P2 E2"
assumes "¬ subsumes P1 C"
assumes "¬ subsumes P2 C"
shows "(Neg E2) ∉ C ∧ (Pos E2) ∉ C"
proof
from ‹C = resolvent_upon P1 P2 E2› have "C = (P1 - { Pos E2 }) ∪ (P2 - { Neg E2 })"
by auto
show "(Neg E2) ∉ C"
proof
assume "Neg E2 ∈ C"
from ‹C = resolvent_upon P1 P2 E2› have "C = (P1 - { Pos E2 }) ∪ (P2 - { Neg E2 })"
by auto
with ‹Neg E2 ∈ C› have "Neg E2 ∈ P1" by auto
from ‹¬ subsumes P1 C› and ‹C = (P1 - { Pos E2 }) ∪ (P2 - { Neg E2 })› have "Pos E2 ∈ P1"
unfolding subsumes_def by auto
from ‹Neg E2 ∈ P1› and ‹Pos E2 ∈ P1› and ‹¬ tautology P1› show "False"
unfolding tautology_def by auto
qed
next show "(Pos E2) ∉ C"
proof
assume "Pos E2 ∈ C"
from ‹C = resolvent_upon P1 P2 E2› have "C = (P1 - { Pos E2 }) ∪ (P2 - { Neg E2 })"
by auto
with ‹Pos E2 ∈ C› have "Pos E2 ∈ P2" by auto
from ‹¬ subsumes P2 C› and ‹C = (P1 - { Pos E2 }) ∪ (P2 - { Neg E2 })› have "Neg E2 ∈ P2"
unfolding subsumes_def by auto
from ‹Neg E2 ∈ P2› and ‹Pos E2 ∈ P2› and ‹¬ tautology P2› show "False"
unfolding tautology_def by auto
qed
qed
text ‹The next lemma shows that partial saturation can be ensured by computing all
(non-redundant) resolvents upon the considered atom.›
lemma ensures_partial_saturation :
assumes "partial_saturation S E2 (S ∪ R)"
assumes "all_fulfill (λx. ¬(tautology x)) S"
assumes "all_fulfill (in_all_resolvents_upon S E2) R"
assumes "all_fulfill (λx. (¬redundant x S)) R"
shows "partial_saturation (S ∪ R) E2 (S ∪ R)"
proof (rule ccontr)
assume "¬ partial_saturation (S ∪ R) E2 (S ∪ R)"
from this obtain P1 P2 C where "P1 ∈ S ∪ R" and "P2 ∈ S ∪ R" and "C = resolvent_upon P1 P2 E2"
and "¬ redundant C (S ∪ R)"
unfolding partial_saturation_def by auto
have "P1 ∈ S"
proof (rule ccontr)
assume "P1 ∉ S"
with ‹P1 ∈ S ∪ R› have "P1 ∈ R" by auto
with assms(3) obtain P1_1 and P1_2 where "P1_1 ∈ S" and "P1_2 ∈ S"
and "P1 = resolvent_upon P1_1 P1_2 E2"
unfolding all_fulfill_def in_all_resolvents_upon_def by auto
from ‹all_fulfill (λx. ¬(tautology x)) S› and ‹P1_1 ∈ S› and ‹P1_2 ∈ S›
have "¬ tautology P1_1" and "¬ tautology P1_2"
unfolding all_fulfill_def by auto
from ‹all_fulfill (λx. (¬redundant x S)) R› and ‹P1 ∈ R› and ‹P1_1 ∈ S› and ‹P1_2 ∈ S›
have "¬ subsumes P1_1 P1" and "¬ subsumes P1_2 P1"
unfolding redundant_def all_fulfill_def by auto
from ‹¬ tautology P1_1› ‹¬ tautology P1_2› ‹¬ subsumes P1_1 P1› and ‹¬ subsumes P1_2 P1›
and ‹P1 = resolvent_upon P1_1 P1_2 E2›
have "(Neg E2) ∉ P1 ∧ (Pos E2) ∉ P1"
using resolvents_do_not_contain_atom [of P1_1 P1_2 P1 E2] by auto
with ‹C = resolvent_upon P1 P2 E2› have "subsumes P1 C" unfolding subsumes_def by auto
with ‹¬ redundant C (S ∪ R)› and ‹P1 ∈ S ∪ R› show "False" unfolding redundant_def
by auto
qed
have "P2 ∈ S"
proof (rule ccontr)
assume "P2 ∉ S"
with ‹P2 ∈ S ∪ R› have "P2 ∈ R" by auto
with assms(3) obtain P2_1 and P2_2 where "P2_1 ∈ S" and "P2_2 ∈ S"
and "P2 = resolvent_upon P2_1 P2_2 E2"
unfolding all_fulfill_def in_all_resolvents_upon_def by auto
from ‹(all_fulfill (λx. ¬(tautology x)) S )› and ‹P2_1 ∈ S› and ‹P2_2 ∈ S›
have "¬ tautology P2_1" and "¬ tautology P2_2"
unfolding all_fulfill_def by auto
from ‹all_fulfill (λx. (¬redundant x S)) R› and ‹P2 ∈ R› and ‹P2_1 ∈ S› and ‹P2_2 ∈ S›
have "¬ subsumes P2_1 P2" and "¬ subsumes P2_2 P2"
unfolding redundant_def all_fulfill_def by auto
from ‹¬ tautology P2_1› ‹¬ tautology P2_2› ‹¬ subsumes P2_1 P2› and ‹¬ subsumes P2_2 P2›
and ‹P2 = resolvent_upon P2_1 P2_2 E2›
have "(Neg E2) ∉ P2 ∧ (Pos E2) ∉ P2"
using resolvents_do_not_contain_atom [of P2_1 P2_2 P2 E2] by auto
with ‹C = resolvent_upon P1 P2 E2› have "subsumes P2 C" unfolding subsumes_def by auto
with ‹¬ redundant C (S ∪ R)› and ‹P2 ∈ S ∪ R›
show "False" unfolding redundant_def by auto
qed
from ‹P1 ∈ S› and ‹P2 ∈ S› and ‹partial_saturation S E2 (S ∪ R)›
and ‹C = resolvent_upon P1 P2 E2› and ‹¬ redundant C (S ∪ R)›
show "False" unfolding redundant_def partial_saturation_def by auto
qed
lemma resolvents_preserve_equivalence:
shows "equivalent S (S ∪ (all_resolvents_upon S A))"
proof -
have "S ⊆ (S ∪ (all_resolvents_upon S A))" by auto
then have "entails_formula (S ∪ (all_resolvents_upon S A)) S" using entailment_subset by auto
have "entails_formula S (S ∪ (all_resolvents_upon S A))"
proof (rule ccontr)
assume "¬entails_formula S (S ∪ (all_resolvents_upon S A))"
from this obtain C where "C ∈ (all_resolvents_upon S A)" and "¬entails S C"
unfolding entails_formula_def using entails_member by auto
from ‹C ∈ (all_resolvents_upon S A)› obtain P1 P2
where "C = resolvent_upon P1 P2 A" and "P1 ∈ S" and "P2 ∈ S"
unfolding all_resolvents_upon_def by auto
from ‹C = resolvent_upon P1 P2 A› and ‹P1 ∈ S› and ‹P2 ∈ S› have "entails S C"
using resolvent_upon_correct by auto
with ‹¬entails S C› show "False" by auto
qed
from ‹entails_formula (S ∪ (all_resolvents_upon S A)) S›
and ‹entails_formula S (S ∪ (all_resolvents_upon S A))›
show ?thesis unfolding equivalent_def by auto
qed
text ‹Given a sequence of atoms, we define a sequence of clauses obtained by resolving upon
each atom successively. Simplification rules are applied at each iteration step.›
fun resolvents_sequence :: "(nat ⇒ 'at) ⇒ 'at Formula ⇒ nat ⇒ 'at Formula"
where
"(resolvents_sequence A S 0) = (simplify S)" |
"(resolvents_sequence A S (Suc N)) =
(simplify ((resolvents_sequence A S N)
∪ (all_resolvents_upon (resolvents_sequence A S N) (A N))))"
text ‹The following lemma states that partial saturation is preserved by simplification.›
lemma redundancy_implies_partial_saturation:
assumes "partial_saturation S1 A S1"
assumes "S2 ⊆ S1"
assumes "all_fulfill (λx. redundant x S2) S1"
shows "partial_saturation S2 A S2"
proof (rule ccontr)
assume "¬partial_saturation S2 A S2"
then obtain P1 P2 C where "P1 ∈ S2" "P2 ∈ S2" and "C = (resolvent_upon P1 P2 A)"
and "¬ redundant C S2"
unfolding partial_saturation_def by auto
from ‹P1 ∈ S2› and ‹S2 ⊆ S1› have "P1 ∈ S1" by auto
from ‹P2 ∈ S2› and ‹S2 ⊆ S1› have "P2 ∈ S1" by auto
from ‹P1 ∈ S1› and ‹P2 ∈ S1› and ‹partial_saturation S1 A S1› and ‹C = resolvent_upon P1 P2 A›
have "redundant C S1" unfolding partial_saturation_def by auto
from ‹¬ redundant C S2› have "¬tautology C" unfolding redundant_def by auto
with ‹redundant C S1› obtain D where "D ∈ S1" and "D ⊆ C"
unfolding redundant_def subsumes_def by auto
from ‹D ∈ S1› and ‹all_fulfill (λx. redundant x S2) S1› have "redundant D S2"
unfolding all_fulfill_def by auto
from ‹¬ tautology C› and ‹D ⊆ C› have "¬ tautology D" unfolding tautology_def by auto
with ‹redundant D S2› obtain E where "E ∈ S2" and "E ⊆ D"
unfolding redundant_def subsumes_def by auto
from ‹E ⊆ D› and ‹D ⊆ C› have "E ⊆ C" by auto
from ‹E ∈ S2› and ‹E ⊆ C› and ‹¬redundant C S2› show "False"
unfolding redundant_def subsumes_def by auto
qed
text ‹The next theorem finally states that the implicate generation algorithm is sound and
complete in the sense that the final clause set in the sequence is exactly the set of prime
implicates of the considered clause set.›
theorem incremental_prime_implication_generation:
assumes "atoms_formula S = { X. ∃I::nat. I < N ∧ X = (A I) }"
assumes "all_fulfill finite S"
shows "(prime_implicates S) = (resolvents_sequence A S N)"
proof -
text ‹We define a set of invariants and show that they are satisfied by all sets in the
above sequence. For the last set in the sequence, the invariants ensure that the clause set is
saturated, which entails the desired property.›
let ?Final = "resolvents_sequence A S N"
text ‹We define some properties and show by induction that they are satisfied by all the
clause sets in the constructed sequence›
let ?equiv_init = "λI.(equivalent S (resolvents_sequence A S I))"
let ?partial_saturation = "λI. (∀J::nat. (J < I
⟶ (partial_saturation (resolvents_sequence A S I) (A J) (resolvents_sequence A S I))))"
let ?no_tautologies = "λI.(all_fulfill (λx. ¬(tautology x)) (resolvents_sequence A S I) )"
let ?atoms_init = "λI.(atoms_formula (resolvents_sequence A S I)
⊆ { X. ∃I::nat. I < N ∧ X = (A I)})"
let ?non_redundant = "λI.(non_redundant (resolvents_sequence A S I))"
let ?finite ="λI. (all_fulfill finite (resolvents_sequence A S I))"
have "∀I. (I ≤ N ⟶ (?equiv_init I) ∧ (?partial_saturation I) ∧ (?no_tautologies I)
∧ (?atoms_init I) ∧ (?non_redundant I) ∧ (?finite I) )"
proof (rule allI)
fix I
show " (I ≤ N
⟶ (?equiv_init I) ∧ (?partial_saturation I) ∧ (?no_tautologies I) ∧ (?atoms_init I)
∧ (?non_redundant I) ∧ (?finite I) )" (is "I ≤ N ⟶ ?P I")
proof (induction I)
text ‹We show that the properties are all satisfied by the initial clause set
(after simplification).›
show "0 ≤ N ⟶ ?P 0"
proof (rule impI)+
assume "0 ≤ N"
let ?R = "resolvents_sequence A S 0"
from ‹all_fulfill finite S›
have "?equiv_init 0" using simplify_preserves_equivalence by auto
moreover have "?no_tautologies 0"
using simplify_def strictly_redundant_def all_fulfill_def by auto
moreover have "?partial_saturation 0" by auto
moreover from ‹all_fulfill finite S› have "?finite 0" using simplify_finite by auto
moreover have "atoms_formula ?R ⊆ atoms_formula S" using atoms_formula_simplify by auto
moreover with ‹atoms_formula S = { X. ∃I::nat. I < N ∧ X = (A I) }›
have v: "?atoms_init 0" unfolding simplify_def by auto
moreover have "?non_redundant 0" using simplify_non_redundant by auto
ultimately show "?P 0" by auto
qed
text ‹We then show that the properties are preserved by induction.›
next
fix I assume "I ≤ N ⟶ ?P I"
show "(Suc I) ≤ N ⟶ (?P (Suc I))"
proof (rule impI)+
assume "(Suc I) ≤ N"
let ?Prec = "resolvents_sequence A S I"
let ?R = "resolvents_sequence A S (Suc I)"
from ‹Suc I ≤ N› and ‹I ≤ N ⟶ ?P I›
have "?equiv_init I" and "?partial_saturation I" and "?no_tautologies I" and "?finite I"
and "?atoms_init I" and "?non_redundant I" by auto
have "equivalent ?Prec (?Prec ∪ (all_resolvents_upon ?Prec (A I)))"
using resolvents_preserve_equivalence by auto
from ‹?finite I› have "all_fulfill finite (?Prec ∪ (all_resolvents_upon ?Prec (A I)))"
using all_resolvents_upon_is_finite by auto
then have "all_fulfill finite (simplify (?Prec ∪ (all_resolvents_upon ?Prec (A I))))"
using simplify_finite by auto
then have "?finite (Suc I)" by auto
from ‹all_fulfill finite (?Prec ∪ (all_resolvents_upon ?Prec (A I)))›
have "equivalent (?Prec ∪ (all_resolvents_upon ?Prec (A I))) ?R"
using simplify_preserves_equivalence by auto
from ‹equivalent ?Prec (?Prec ∪ (all_resolvents_upon ?Prec (A I)))›
and ‹equivalent (?Prec ∪ (all_resolvents_upon ?Prec (A I))) ?R›
have "equivalent ?Prec ?R" by (rule equivalent_transitive)
from ‹?equiv_init I› and this have "?equiv_init (Suc I)" by (rule equivalent_transitive)
have "?no_tautologies (Suc I)" using simplify_def strictly_redundant_def all_fulfill_def
by auto
let ?Delta = "?R - ?Prec"
have "?R ⊆ ?Prec ∪ ?Delta" by auto
have "all_fulfill (λx. (redundant x ?R)) (?Prec ∪ ?Delta)"
proof (rule ccontr)
assume "¬all_fulfill (λx. (redundant x ?R)) (?Prec ∪ ?Delta)"
then obtain x where "¬redundant x ?R" and "x ∈ ?Prec ∪ ?Delta" unfolding all_fulfill_def
by auto
from ‹¬redundant x ?R› have "¬x ∈ ?R" unfolding redundant_def subsumes_def by auto
with ‹x ∈ ?Prec ∪ ?Delta› have "x ∈ (?Prec ∪ (all_resolvents_upon ?Prec (A I)))"
by auto
with ‹all_fulfill finite (?Prec ∪ (all_resolvents_upon ?Prec (A I)))›
have "redundant x (simplify (?Prec ∪ (all_resolvents_upon ?Prec (A I))))"
using simplify_and_membership by blast
with ‹¬redundant x ?R› show "False" by auto
qed
have "all_fulfill (in_all_resolvents_upon ?Prec (A I)) ?Delta"
proof (rule ccontr)
assume "¬ (all_fulfill (in_all_resolvents_upon ?Prec (A I)) ?Delta)"
then obtain C where "C ∈ ?Delta"
and "¬in_all_resolvents_upon ?Prec (A I) C"
unfolding all_fulfill_def by auto
then obtain C where "C ∈ ?Delta"
and not_res: "∀ P1 P2. ¬(P1 ∈ ?Prec ∧ P2 ∈ ?Prec ∧ C = resolvent_upon P1 P2 (A I))"
unfolding all_fulfill_def in_all_resolvents_upon_def by blast
from ‹C ∈ ?Delta› have "C ∈ ?R" and "C ∉ ?Prec" by auto
then have "C ∈ simplify (?Prec ∪ (all_resolvents_upon ?Prec (A I)))" by auto
then have "C ∈ ?Prec ∪ (all_resolvents_upon ?Prec (A I))" unfolding simplify_def by auto
with ‹C ∉ ?Prec› have "C ∈ (all_resolvents_upon ?Prec (A I))" by auto
with not_res show "False" unfolding all_resolvents_upon_def by auto
qed
have "all_fulfill (λx. (¬redundant x ?Prec)) ?Delta"
proof (rule ccontr)
assume "¬all_fulfill (λx. (¬redundant x ?Prec)) ?Delta"
then obtain C where "C ∈ ?Delta" and redundant: "redundant C ?Prec"
unfolding all_fulfill_def by auto
from ‹C ∈ ?Delta› have "C ∈ ?R" and "C ∉ ?Prec" by auto
show "False"
proof cases
assume "strictly_redundant C ?Prec"
then have "strictly_redundant C (?Prec ∪ (all_resolvents_upon ?Prec (A I)))"
unfolding strictly_redundant_def by auto
then have "C ∉ simplify (?Prec ∪ (all_resolvents_upon ?Prec (A I)))"
unfolding simplify_def by auto
then have "C ∉ ?R" by auto
with ‹C ∈ ?R› show "False" by auto
next assume "¬strictly_redundant C ?Prec"
with redundant have "C ∈ ?Prec"
unfolding strictly_redundant_def redundant_def subsumes_def by auto
with ‹C ∉ ?Prec› show "False" by auto
qed
qed
have "∀J::nat. (J < (Suc I)) ⟶ (partial_saturation ?R (A J) ?R)"
proof (rule ccontr)
assume "¬(∀J::nat. (J < (Suc I)) ⟶ (partial_saturation ?R (A J) ?R))"
then obtain J where "J < (Suc I)" and "¬(partial_saturation ?R (A J) ?R)" by auto
from ‹¬(partial_saturation ?R (A J) ?R)› obtain P1 P2 C
where "P1 ∈ ?R" and "P2 ∈ ?R" and "C = resolvent_upon P1 P2 (A J)" and "¬ redundant C ?R"
unfolding partial_saturation_def by auto
have "partial_saturation ?Prec (A I) (?Prec ∪ ?Delta)"
proof (rule ccontr)
assume "¬partial_saturation ?Prec (A I) (?Prec ∪ ?Delta)"
then obtain P1 P2 C where "P1 ∈ ?Prec" and "P2 ∈ ?Prec"
and "C = resolvent_upon P1 P2 (A I)" and
"¬redundant C (?Prec ∪ ?Delta)" unfolding partial_saturation_def by auto
from ‹C = resolvent_upon P1 P2 (A I)› and ‹P1 ∈ ?Prec› and ‹P2 ∈ ?Prec›
have "C ∈ ?Prec ∪ (all_resolvents_upon ?Prec (A I))"
unfolding all_resolvents_upon_def by auto
from ‹all_fulfill finite (?Prec ∪ (all_resolvents_upon ?Prec (A I)))›
and this have "redundant C ?R"
using simplify_and_membership [of "?Prec ∪ (all_resolvents_upon ?Prec (A I))" ?R C]
by auto
with ‹?R ⊆ ?Prec ∪ ?Delta› have "redundant C (?Prec ∪ ?Delta)"
using superset_preserves_redundancy [of C ?R "(?Prec ∪ ?Delta)"] by auto
with ‹¬redundant C (?Prec ∪ ?Delta)› show "False" by auto
qed
show "False"
proof cases
assume "J = I"
from ‹partial_saturation ?Prec (A I) (?Prec ∪ ?Delta)› and ‹?no_tautologies I›
and ‹(all_fulfill (in_all_resolvents_upon ?Prec (A I)) ?Delta)›
and ‹all_fulfill (λx. (¬redundant x ?Prec)) ?Delta›
have "partial_saturation (?Prec ∪ ?Delta) (A I) (?Prec ∪ ?Delta)"
using ensures_partial_saturation [of ?Prec "(A I)" ?Delta] by auto
with ‹?R ⊆ ?Prec ∪ ?Delta›
and ‹all_fulfill (λx. (redundant x ?R)) (?Prec ∪ ?Delta)›
have "partial_saturation ?R (A I) ?R" using redundancy_implies_partial_saturation
by auto
with ‹J = I› and ‹¬(partial_saturation ?R (A J) ?R)› show "False" by auto
next
assume "J ≠ I"
with ‹J < (Suc I)› have "J < I" by auto
with ‹?partial_saturation I›
have "partial_saturation ?Prec (A J) ?Prec" by auto
with ‹partial_saturation ?Prec (A I) (?Prec ∪ ?Delta)› and ‹?no_tautologies I›
and ‹(all_fulfill (in_all_resolvents_upon ?Prec (A I)) ?Delta)›
and ‹all_fulfill (λx. (¬redundant x ?Prec)) ?Delta›
have "partial_saturation (?Prec ∪ ?Delta) (A J) (?Prec ∪ ?Delta)"
using partial_saturation_is_preserved [of ?Prec "A J" "A I" ?Delta] by auto
with ‹?R ⊆ ?Prec ∪ ?Delta›
and ‹all_fulfill (λx. (redundant x ?R)) (?Prec ∪ ?Delta)›
have "partial_saturation ?R (A J) ?R"
using redundancy_implies_partial_saturation by auto
with ‹¬(partial_saturation ?R (A J) ?R)› show "False" by auto
qed
qed
have "non_redundant ?R" using simplify_non_redundant by auto
from ‹?atoms_init I› have "atoms_formula (all_resolvents_upon ?Prec (A I))
⊆ { X. ∃I::nat. I < N ∧ X = (A I)}"
using atoms_formula_resolvents [of ?Prec "A I"] by auto
with ‹?atoms_init I›
have "atoms_formula (?Prec ∪ (all_resolvents_upon ?Prec (A I)))
⊆ { X. ∃I::nat. I < N ∧ X = (A I)}"
using atoms_formula_union [of ?Prec "all_resolvents_upon ?Prec (A I)"] by auto
from this have "atoms_formula ?R ⊆ { X. ∃I::nat. I < N ∧ X = (A I)}"
using atoms_formula_simplify [of "?Prec ∪ (all_resolvents_upon ?Prec (A I))"] by auto
from ‹equivalent S (resolvents_sequence A S (Suc I))›
and ‹(∀J::nat. (J < (Suc I)
⟶ (partial_saturation (resolvents_sequence A S (Suc I)) (A J)
(resolvents_sequence A S (Suc I)))))›
and ‹(all_fulfill (λx. ¬(tautology x)) (resolvents_sequence A S (Suc I)) )›
and ‹(all_fulfill finite (resolvents_sequence A S (Suc I)))›
and ‹non_redundant ?R›
and ‹atoms_formula (resolvents_sequence A S (Suc I)) ⊆ { X. ∃I::nat. I < N ∧ X = (A I)}›
show "?P (Suc I)" by auto
qed
qed
qed
text ‹Using the above invariants, we show that the final clause set is saturated.›
from this have "∀J. (J < N ⟶ partial_saturation ?Final (A J) ?Final)"
and "atoms_formula (resolvents_sequence A S N) ⊆ { X. ∃I::nat. I < N ∧ X = (A I)}"
and "equivalent S ?Final"
and "non_redundant ?Final"
and "all_fulfill finite ?Final"
by auto
have "saturated_binary_rule resolvent ?Final"
proof (rule ccontr)
assume "¬ saturated_binary_rule resolvent ?Final"
then obtain P1 P2 C where "P1 ∈ ?Final" and "P2 ∈ ?Final" and "resolvent P1 P2 C"
and "¬redundant C ?Final"
unfolding saturated_binary_rule_def by auto
from ‹resolvent P1 P2 C› obtain B where "C = resolvent_upon P1 P2 B"
unfolding resolvent_def by auto
show "False"
proof cases
assume "B ∈ (atoms_formula ?Final)"
with ‹atoms_formula ?Final ⊆ { X. ∃I::nat. I < N ∧ X = (A I) }›
obtain I where "B = (A I)" and "I < N"
by auto
from ‹B = (A I)› and ‹C = resolvent_upon P1 P2 B› have "C = resolvent_upon P1 P2 (A I)"
by auto
from ‹∀J. (J < N ⟶ partial_saturation ?Final (A J) ?Final)› and ‹B = (A I)›and ‹I < N›
have "partial_saturation ?Final (A I) ?Final" by auto
with ‹C = resolvent_upon P1 P2 (A I)›and ‹P1 ∈ ?Final› and ‹P2 ∈ ?Final›
have "redundant C ?Final" unfolding partial_saturation_def by auto
with ‹¬redundant C ?Final› show "False" by auto
next
assume "B ∉ atoms_formula ?Final"
with ‹P1 ∈ ?Final› have "B ∉ atoms_clause P1" by auto
then have "Pos B ∉ P1" by auto
with ‹C = resolvent_upon P1 P2 B› have "P1 ⊆ C" by auto
with ‹P1 ∈ ?Final› and ‹¬redundant C ?Final› show "False"
unfolding redundant_def subsumes_def by auto
qed
qed
with ‹all_fulfill finite ?Final› and ‹non_redundant ?Final›
have "prime_implicates ?Final = ?Final"
using prime_implicates_of_saturated_sets [of ?Final] by auto
with ‹equivalent S ?Final› show ?thesis using equivalence_and_prime_implicates by auto
qed
end
end