Core Chase Trees

Next to the CoreChaseBranch definition, we also define a tree version in line with what is done for our generic and regular chase structures.

@[reducible, inline]

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

Equations

• CoreTreeDerivation rules = TreeDerivation (CoreChaseNode rules) (RestrictedObsolescence sig) rules

Finiteness of FactSets in the Core Chase

If we start a CoreTreeDerivation 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 CoreTreeDerivation.

theorem CoreTreeDerivation.facts_finite_of_mem_of_root_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (root_fin : Set.finite (TreeDerivation.root td).facts) (node : TreeDerivation.NodeWithAddress td) : Set.finite node.node.facts

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

theorem CoreTreeDerivation.core_finite_of_mem_of_root_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (root_fin : Set.finite (TreeDerivation.root td).core) (node : TreeDerivation.NodeWithAddress td) : Set.finite node.node.core

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

Homomorphisms along the Chase

In the regular TreeDerivation, 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 following fact sets. (This trivially holds for the regular tree derivation as well since with the subset relation the id mapping always forms such a homomorphism.)

theorem CoreTreeDerivation.exists_homomorphism_from_root_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (node : CoreChaseNode rules) : node ∈ td → ∃ (h : GroundTermMapping sig), h.isHomomorphism (TreeDerivation.root td).core node.core

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

theorem CoreTreeDerivation.root_core_not_mem_childTrees_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (root_finite : Set.finite (TreeDerivation.root td).core) (c : TreeDerivation (CoreChaseNode rules) (RestrictedObsolescence sig) rules) : c ∈ TreeDerivation.childTrees td → ∀ (node : CoreChaseNode rules), node ∈ c → (TreeDerivation.root td).core ≠ node.core

The root's core cannot occur again in the child trees. 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 TreeDerivations but the argument is easier for them.

theorem CoreTreeDerivation.root_not_mem_childTrees_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (root_finite : Set.finite (TreeDerivation.root td).core) : ¬∃ (t : TreeDerivation (CoreChaseNode rules) (RestrictedObsolescence sig) rules), t ∈ TreeDerivation.childTrees td ∧ TreeDerivation.root td ∈ t

The root cannot occur in the childTrees. 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 TreeDerivations but the argument is easier for them.

theorem CoreTreeDerivation.eq_of_suffix_of_root_mem_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td1 td2 : CoreTreeDerivation rules} (suffix : td1 <:+ td2) (root_mem : TreeDerivation.root td2 ∈ td1) (root_finite : Set.finite (TreeDerivation.root td2).core) : td1 = td2

By root_not_mem_childTrees_of_finite, if we have a subtree but our root occurs in the subtree, then our subtree is equal to us.

Predecessor Relation

We port the predecessor results from the TreeDerivation that are there only shown for derivations with RegularChaseNodes.

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 RegularTreeDerivation.facts_not_subset_of_strict_predecessor.

theorem CoreTreeDerivation.exists_homomorphism_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} {n1 n2 : TreeDerivation.NodeWithAddress td} : n1 ≼ n2 → ∃ (h : GroundTermMapping sig), h.isHomomorphism n1.node.core n2.node.core

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

theorem CoreTreeDerivation.node_strict_prec_childNodes_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (root_fin : Set.finite (TreeDerivation.root td).core) {node : TreeDerivation.NodeWithAddress td} (c : TreeDerivation.NodeWithAddress td) : c ∈ node.childNodes → node ≺ c

The node is a strict predecessor of each of its childNodes.

theorem CoreTreeDerivation.core_not_subset_of_strict_predecessor_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} {n1 n2 : TreeDerivation.NodeWithAddress td} (n1_fin : Set.finite n1.node.core) : n1 ≺ n2 → ¬n2.node.core ⊆ n1.node.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 CoreTreeDerivation.constants_node_subset_constants_fs_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td child : CoreTreeDerivation rules} (child_mem : child ∈ TreeDerivation.childTrees td) {node : CoreChaseNode rules} (node_mem : node ∈ child) : node.facts.constants ⊆ (TreeDerivation.root td).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 CoreTreeDerivation.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td child : CoreTreeDerivation rules} (child_mem : child ∈ TreeDerivation.childTrees td) (node : TreeDerivation.NodeWithAddress child) {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.node.facts.terms) : t ∈ (TreeDerivation.root td).core.terms ∨ ∃ (node2 : TreeDerivation.NodeWithAddress child), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.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 CoreTreeDerivation.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td child : CoreTreeDerivation rules} (child_mem : child ∈ TreeDerivation.childTrees td) (node : TreeDerivation.NodeWithAddress child) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.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 ∈ (TreeDerivation.root td).core.terms ∨ ∃ (node2 : TreeDerivation.NodeWithAddress child), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.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 tree derivations, the result of a core tree derivation is only defined if the derivation terminates. Then it is simply the last element. Just like for RegularTreeDerivations however, the result also models all rules.

@[reducible, inline]

abbrev CoreTreeDerivation.result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} (td : CoreTreeDerivation rules) (term : TreeDerivation.terminates td) : Set (FactSet sig)

Equations

• td.result term fs = ∃ (deriv : CoreChaseDerivation rules), ∃ (mem : deriv ∈ TreeDerivation.branches td), deriv.result ⋯ = fs

theorem CoreTreeDerivation.result_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (term : TreeDerivation.terminates td) : (td.result term).finite

Since the result is only defined for terminating trees, it must be finite (which does not mean that each individual fact set is finite as well, this would only hold for proper CoreChaseTrees).

theorem CoreTreeDerivation.result_models_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {td : CoreTreeDerivation rules} (term : TreeDerivation.terminates td) (fs : FactSet sig) : fs ∈ td.result term → fs.modelsRules rules

Each element of the result models the rules.

@[reducible, inline]

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

Equations

• CoreChaseTree kb = ChaseTree (CoreChaseNode kb.rules) (RestrictedObsolescence sig) kb

Finiteness of FactSets in the Core Chase

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

theorem CoreChaseTree.facts_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} (node : ct.NodeWithAddress) : Set.finite node.node.facts

theorem CoreChaseTree.core_finite_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} (node : ct.NodeWithAddress) : Set.finite node.node.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. We also have a result here stating that every member of the CoreChaseTree result is a model.

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

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

theorem CoreChaseTree.result_models_kb {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} (term : ct.terminates) (fs : FactSet sig) : fs ∈ CoreTreeDerivation.result ct.toTreeDerivation term → fs.modelsKb kb

Each result member of a CoreChaseTree models the whole KnowledgeBase.

Predecessor Relation

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

theorem CoreChaseTree.node_strict_prec_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} {node : ct.NodeWithAddress} (c : ct.NodeWithAddress) : c ∈ node.childNodes → node ≺ c

The node is a strict predecessor of each of its childNodes.

theorem CoreChaseTree.core_not_subset_of_strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} {n1 n2 : ct.NodeWithAddress} : n1 ≺ n2 → ¬n2.node.core ⊆ n1.node.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 CoreChaseTree.constants_node_subset_constants_db_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} {node : CoreChaseNode kb.rules} (node_mem : node ∈ ct) : node.facts.constants ⊆ kb.db.constants.val ∪ kb.rules.head_constants

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

theorem CoreChaseTree.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} (node : ct.NodeWithAddress) {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.node.facts.terms) : ∃ (node2 : ct.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.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 CoreChaseTree.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} {ct : CoreChaseTree kb} (node : ct.NodeWithAddress) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.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 : ct.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } kb.rules) × Fin trg.val.rule.head.length), orig ∈ node2.node.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.

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 trees this is trivial because of fact monotonicity but here it is not quite obvious (even though it's intuitive).

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