Core Chase Derivations and Branches

Similar to RegularChaseDerivations and RegularChaseBranches, we define CoreChaseDerivations and CoreChaseBranches. The main result of this file is that the result of a CoreChaseBranch models the underlying KnowledgeBase.

@[reducible, inline]

abbrev CoreChaseDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rules : RuleSet sig) : Type (max (max u_3 u_2) u_1)

Equations

• CoreChaseDerivation rules = ChaseDerivation (CoreChaseNode rules) (RestrictedObsolescence sig) rules

Finiteness of FactSets in the Core Chase

If we start a CoreChaseDerivation on a finite fact set, all other fact sets (and cores) also remain finite. For regular chase derivations, we only show this for ChaseBranches that start on a database. However, here we also require such a result on auxiliary results that we show for the CoreChaseDerivation.

theorem CoreChaseDerivation.facts_finite_of_mem_of_head_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (head_fin : Set.finite cd.head.facts) (node : ChaseDerivation.Node cd) : Set.finite node.val.facts

If the initial facts are finite, then the facts of every node are finite.

theorem CoreChaseDerivation.core_finite_of_mem_of_head_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (head_fin : Set.finite cd.head.core) (node : ChaseDerivation.Node cd) : Set.finite node.val.core

If the initial core is finite, then the cores of every node are finite.

Homomorphisms along the Chase

In the regular ChaseDerivation, each steps can only add facts, which makes consecutive nodes subsets of each other. This is not true for the core chase. But at least, we can always find a homomorphism into the next fact set. (This trivially holds for the regular chase derivation as well since with the subset relation the id mapping always forms such a homomorphism.)

theorem CoreChaseDerivation.exists_homomorphism_from_head_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (node : CoreChaseNode rules) : node ∈ cd → ∃ (h : GroundTermMapping sig), h.isHomomorphism cd.head.core node.core

For each derivation, there is a homomorphism from its head into every node.

theorem CoreChaseDerivation.head_core_not_mem_tail_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (head_finite : Set.finite cd.head.core) (h : cd.next.isSome = true) (node : CoreChaseNode rules) : node ∈ ChaseDerivation.tail cd h → cd.head.core ≠ node.core

The head's core cannot occur again in the tail. If this was the case and since we always find homomorphism from to successor cores, we can argue that then the triggers would have already been satisfied. The same theorem exists for regular ChaseDerivations but the argument is easier for them.

theorem CoreChaseDerivation.head_not_mem_tail_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (head_finite : Set.finite cd.head.core) (h : cd.next.isSome = true) : ¬cd.head ∈ ChaseDerivation.tail cd h

The head cannot occur in the tail. Otherwise, the same fact set would occur twice in the chase. But since we always find homomorphism from to successor fact sets, we can argue that then the triggers would have already been satisfied. The same theorem exists for regular ChaseDerivations but the argument is easier for them.

theorem CoreChaseDerivation.eq_of_suffix_of_head_mem_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd1 cd2 : CoreChaseDerivation rules} (suffix : cd1 <:+ cd2) (head_mem : cd2.head ∈ cd1) (head_finite : Set.finite cd2.head.core) : cd1 = cd2

By head_not_mem_tail_of_finite, if we have a suffix but our head occurs in the suffix, then our suffix is equal to us.

theorem CoreChaseDerivation.suffix_of_suffix_of_suffix_of_head_mem_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd cd1 cd2 : CoreChaseDerivation rules} : cd1 <:+ cd → cd2 <:+ cd → cd2.head ∈ cd1 → Set.finite cd2.head.core → cd2 <:+ cd1

And now by eq_of_suffix_of_head_mem_of_finite, if we have two suffixes $C$ and $D$, and the head of $D$ occurs in $C$, then $D$ is a suffix of $C$. This also holds for regular chase derivations but for different reasons (see the differences of head_not_mem_tail_of_finite and ChaseDerivation.head_not_mem_tail.)

Predecessor Relation

We port the predecessor results from the ChaseDerivation that are there only shown for derivations with RegularChaseNodes. But since we have suffix_of_suffix_of_suffix_of_head_mem_of_finite, we can also show these for CoreChaseDerivations given that the cores are finite.

We also add a few results on top that are specific to the core chase such as exists_homomorphism_of_prec or core_not_subset_of_strict_predecessor (where the latter is a variant of ChaseDerivation.facts_not_subset_of_strict_predecessor.

theorem CoreChaseDerivation.predecessor_antisymm_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 : ChaseDerivation.Node cd} (n1_fin : Set.finite n1.val.core) (n2_fin : Set.finite n2.val.core) : n1 ≼ n2 → n2 ≼ n1 → n1 = n2

The predecessor relation is antisymmetric.

theorem CoreChaseDerivation.predecessor_trans_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 n3 : ChaseDerivation.Node cd} (n2_fin : Set.finite n2.val.core) : n1 ≼ n2 → n2 ≼ n3 → n1 ≼ n3

The predecessor relation is transitive.

theorem CoreChaseDerivation.fairness_prec_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (head_fin : Set.finite cd.head.core) (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) : ∃ (node : ChaseDerivation.Node cd), ∀ (node2 : cd.Node), node ≼ node2 → ¬trg.val.active node2.val.core

We can express fairness in terms of the predecessor relation: For each trigger, there is a node such that the trigger is not active for each of the node's successors.

theorem CoreChaseDerivation.exists_homomorphism_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 : ChaseDerivation.Node cd} : n1 ≼ n2 → ∃ (h : GroundTermMapping sig), h.isHomomorphism n1.val.core n2.val.core

For each node, there exists a homomorphism to each of its successors.

theorem CoreChaseDerivation.strict_predecessor_asymmetric_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 : ChaseDerivation.Node cd} (n1_fin : Set.finite n1.val.core) (n2_fin : Set.finite n2.val.core) : n1 ≺ n2 → ¬n2 ≺ n1

The strict predecessor relation is asymmetric.

theorem CoreChaseDerivation.strict_predecessor_trans_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 n3 : ChaseDerivation.Node cd} (n1_fin : Set.finite n1.val.core) (n2_fin : Set.finite n2.val.core) : n1 ≺ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive.

theorem CoreChaseDerivation.strict_prec_of_prec_of_strict_prec_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 n3 : ChaseDerivation.Node cd} (n1_fin : Set.finite n1.val.core) (n2_fin : Set.finite n2.val.core) : n1 ≼ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive with respect to the regular predecessor relation.

theorem CoreChaseDerivation.strict_prec_of_strict_prec_of_prec_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 n3 : ChaseDerivation.Node cd} (n1_fin : Set.finite n1.val.core) (n2_fin : Set.finite n2.val.core) : n1 ≺ n2 → n2 ≼ n3 → n1 ≺ n3

The strict predecessor relation is transitive with respect to the regular predecessor relation.

theorem CoreChaseDerivation.head_strict_prec_next_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (head_fin : Set.finite cd.head.core) {next : CoreChaseNode rules} (mem : next ∈ cd.next) : ⟨cd.head, ⋯⟩ ≺ ⟨next, ⋯⟩

The ChaseDerivationSkeleton.head is a strict predecessor of ChaseDerivationSkeleton.next.

theorem CoreChaseDerivation.core_not_subset_of_strict_predecessor_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {n1 n2 : ChaseDerivation.Node cd} (n1_fin : Set.finite n1.val.core) : n1 ≺ n2 → ¬n2.val.core ⊆ n1.val.core

The core of a strict successor cannot be a subset of our core. Otherwise, our current core would not be a core.

Terms in the Chase

We make some general observations about certain terms that might occur in the chase.

1. Constants can only originate directly from rules or from the initial fact set. No other constants can be introduced.
2. Functional terms can either also originate from the initial fact set or they are introduced as fresh terms by a trigger.

The second observation entails that the precense of a functional term that does not occur in the initial fact set implies that the trigger that introduces this term must have been applied in some ChaseNode.

theorem CoreChaseDerivation.constants_node_subset_constants_fs_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {next_some : cd.next.isSome = true} {node : CoreChaseNode rules} (node_mem : node ∈ ChaseDerivation.tail cd next_some) : node.facts.constants ⊆ cd.head.core.constants ∪ rules.head_constants

Constants in the chase can only come from the initial fact set or from a constant in a rule.

theorem CoreChaseDerivation.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {next_some : cd.next.isSome = true} (start_finite : Set.finite cd.head.core) (node : (ChaseDerivation.tail cd next_some).Node) {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) (t_mem : t ∈ node.val.facts.terms) : t ∈ cd.head.core.terms ∨ ∃ (node2 : (ChaseDerivation.tail cd next_some).Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ node2.val.origin ∧ t ∈ orig.fst.val.fresh_terms_for_head_disjunct ↑orig.snd ⋯

Each functional term in the chase originates as a fresh term from a trigger if it was not already part of the initial fact set.

theorem CoreChaseDerivation.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} {next_some : cd.next.isSome = true} (start_finite : Set.finite cd.head.core) (node : (ChaseDerivation.tail cd next_some).Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.facts.terms) {trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ cd.head.core.terms ∨ ∃ (node2 : (ChaseDerivation.tail cd next_some).Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ node2.val.origin ∧ orig.fst.equiv trg ∧ ↑orig.snd = disj_idx

If a functional term occurs in the chase, then the trigger that introduces this term must have been used in the chase, unless the term already occurs in the initial fact set.

Core Chase Result

Oppossed to regular chase derivations, the result of a core chase derivation is only defined if the derivation terminates. Then it is simply the last element. Just like for RegularChaseDerivations however, the result also models all rules.

@[reducible, inline]

abbrev CoreChaseDerivation.result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} (cd : CoreChaseDerivation rules) (term : ChaseDerivation.terminates cd) : FactSet sig

Equations

• cd.result term = (cd.last term).core

theorem CoreChaseDerivation.result_models_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {cd : CoreChaseDerivation rules} (term : ChaseDerivation.terminates cd) : (cd.result term).modelsRules rules

The result is a model of all rules. This is true because otherwise, there would be an active trigger on the result. But we already know that no trigger can be active on the last node of a terminating chase derivation.

@[reducible, inline]

abbrev CoreChaseBranch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (kb : KnowledgeBase sig) : Type (max (max u_3 u_2) u_1)

Equations

• CoreChaseBranch kb = ChaseBranch (CoreChaseNode kb.rules) (RestrictedObsolescence sig) kb

Finiteness of FactSets in the Core Chase

Just as in a regular ChaseBranch, every fact set (and every core) that occurs in the CoreChaseBranch is finite simply since the (initial) database is finite and since each step only adds finitely many facts.

theorem CoreChaseBranch.facts_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (node : cb.Node) : Set.finite node.val.facts

theorem CoreChaseBranch.core_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (node : cb.Node) : Set.finite node.val.core

Database Containment

Even though we do not have fact set monotonicity in the core chase, it is still true that the database occurs in every fact set and core in the chase. This is because the database only features constants and these can never be remapped by any homomorphism. This result is essential for showing that the core chase result is a model, which we also show here.

theorem CoreChaseBranch.db_mem_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (node : cb.Node) : kb.db.toFactSet.val ⊆ node.val.core

The database is a subset of each node since the database only contains constants which can never be remapped by homomorphisms.

theorem CoreChaseBranch.result_models_kb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (term : cb.terminates) : (CoreChaseDerivation.result cb.toChaseDerivation term).modelsKb kb

The result of a CoreChaseBranch models the whole KnowledgeBase.

Predecessor Relation

Compared to the CoreChaseDerivation, we can now drop the explicit finiteness conditions.

theorem CoreChaseBranch.predecessor_antisymm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 : cb.Node} : n1 ≼ n2 → n2 ≼ n1 → n1 = n2

The predecessor relation is antisymmetric.

theorem CoreChaseBranch.predecessor_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 n3 : cb.Node} : n1 ≼ n2 → n2 ≼ n3 → n1 ≼ n3

The predecessor relation is transitive.

theorem CoreChaseBranch.fairness_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules) : ∃ (node : cb.Node), ∀ (node2 : cb.Node), node ≼ node2 → ¬trg.val.active node2.val.core

We can express fairness in terms of the predecessor relation: For each trigger, there is a node such that the trigger is not active for each of the node's successors.

theorem CoreChaseBranch.strict_predecessor_asymmetric {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 : cb.Node} : n1 ≺ n2 → ¬n2 ≺ n1

The strict predecessor relation is asymmetric.

theorem CoreChaseBranch.strict_predecessor_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 n3 : cb.Node} : n1 ≺ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive.

theorem CoreChaseBranch.strict_prec_of_prec_of_strict_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 n3 : cb.Node} : n1 ≼ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive with respect to the regular predecessor relation.

theorem CoreChaseBranch.strict_prec_of_strict_prec_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 n3 : cb.Node} : n1 ≺ n2 → n2 ≼ n3 → n1 ≺ n3

The strict predecessor relation is transitive with respect to the regular predecessor relation.

theorem CoreChaseBranch.head_strict_prec_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {next : CoreChaseNode kb.rules} (mem : next ∈ cb.next) : ⟨cb.head, ⋯⟩ ≺ ⟨next, ⋯⟩

The ChaseDerivationSkeleton.head is a strict predecessor of ChaseDerivationSkeleton.next.

theorem CoreChaseBranch.core_not_subset_of_strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 : cb.Node} : n1 ≺ n2 → ¬n2.val.core ⊆ n1.val.core

The core of a strict successor cannot be a subset of our core. Otherwise, our current core would not be a core.

theorem CoreChaseBranch.wellFounded_pred {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} : WellFounded ChaseDerivationSkeleton.strict_predecessor

The strict_predecessor relation is WellFounded.

@[instance_reducible]

instance CoreChaseBranch.instWellFoundedRelationNodeRulesCoreChaseNode {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} : WellFoundedRelation cb.Node

Equations

• CoreChaseBranch.instWellFoundedRelationNodeRulesCoreChaseNode = { rel := ChaseDerivationSkeleton.strict_predecessor, wf := ⋯ }

Terms in the Chase

We make some general observations about certain terms that might occur in the chase.

1. Constants can only originate directly from rules or from the initial fact set. No other constants can be introduced.
2. Functional terms can either also originate from the initial fact set or they are introduced as fresh terms by a trigger.

The second observation entails that the precense of a functional term that does not occur in the initial fact set implies that the trigger that introduces this term must have been applied in some ChaseNode.

theorem CoreChaseBranch.constants_node_subset_constants_db_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {node : cb.Node} : node.val.facts.constants ⊆ kb.db.constants.val ∪ kb.rules.head_constants

Constants in the chase must be in the database or in some rule.

theorem CoreChaseBranch.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (node : cb.Node) {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) (t_mem : t ∈ node.val.facts.terms) : ∃ (node2 : cb.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ node2.val.origin ∧ t ∈ orig.fst.val.fresh_terms_for_head_disjunct ↑orig.snd ⋯

Each functional term in the chase originates as a fresh term from a trigger.

theorem CoreChaseBranch.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} (node : cb.Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.facts.terms) {trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : ∃ (node2 : cb.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ node2.val.origin ∧ orig.fst.equiv trg ∧ ↑orig.snd = disj_idx

If a functional term occurs in the chase, then the trigger that introduces this term must have been used in the chase.

Minimal Nodes with given Properties

If a property hold for a given node in the chase, then there must be a "first" node for which this property holds. That means that this node is minimal with respect to the ≺ relation. The result follows by the well foundedness of the ≺ relation.

theorem CoreChaseBranch.prop_for_node_has_minimal_such_node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cd : CoreChaseBranch kb} (prop : cd.Node → Prop) (n : cd.Node) : prop n → ∃ (n2 : cd.Node), prop n2 ∧ n2 ≼ n ∧ ∀ (n3 : cd.Node), n3 ≺ n2 → ¬prop n3

Used triggers remain inactive

Here we prove that triggers used in the core chase remain inactive from this point. Not only that but also every equivalent trigger (producing the same result) is inactive from this point on. For regular chase derivations this is trivial because of fact monotonicity but here it is not quite obvious (even though it's intuitive).

theorem CoreChaseBranch.origin_trg_remains_inactive {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {cb : CoreChaseBranch kb} {n1 n2 : cb.Node} (prec : n1 ≼ n2) (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length) : orig ∈ n1.val.origin → ∀ (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules), orig.fst.equiv trg → ¬trg.val.active n2.val.core