Core Chase Node

Similar to a ChaseNode, we define another elements of the core chase in a similar fashion. Besides fact set and origin, these also store the core that the fact set is being condensed to. In principle any such core is allowed and we do not enforce a specific computation procedure.

Homomorphism Repetition in homSubsets

As a very general insight we prove that we can repeat a homomorphism from a homSubset relation such that the repeated mapping is still a homomorphism but at the same time the id on all terms that occur in the subset. This works if the subset is finite.

theorem ex_hom_that_is_id_on_terms_of_isWeakCore_of_homSubset_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs core : FactSet sig} (wc : core.isWeakCore) (homSub : core.homSubset fs) (fin : Set.finite core) : ∃ (h : GroundTermMapping sig), h.isHomomorphism fs core ∧ ∀ (t : GroundTerm sig), t ∈ core.terms → h t = t

If core is a finite weak core and a homSubset of fs, then there is a homomorphism from fs to core that is the identity on all of core's terms.

Trigger Satisfaction along finite homSubsets.

Given a few extra conditions, trigger satisfaction is preserved along the homSubset relation. This is helpful for the CoreChaseNode later on as each node features a homSubset internally.

theorem trg_remains_obsolete_of_isWeakCore_of_homSubset_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs core : FactSet sig} (wc : core.isWeakCore) (homSub : core.homSubset fs) (fin : Set.finite core) (trg : PreTrigger sig) : trg.satisfied fs → trg.mapped_frontier.toSet ⊆ core.terms → trg.satisfied core

If a trigger is satisfied for fs and all of its frontier terms still occur in a finite core homSubset of fs, then the trigger is also satisfied in this homSubset.

theorem equiv_trg_obsolete_of_isWeakCore_of_homSubset_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {fs core : FactSet sig} (wc : core.isWeakCore) (homSub : core.homSubset fs) (fin : Set.finite core) (trg : PreTrigger sig) : trg.satisfied fs → ∀ (trg2 : PreTrigger sig), trg.equiv trg2 → trg2.loaded core → trg2.satisfied core

If a trigger is satisfied for fs, for every core homSubset of fs, every equivalent trigger is satisfied given that is is loaded. This is a direct consequence of trg_remains_obsolete_of_isWeakCore_of_homSubset_of_finite.

CoreChaseNode Definition and Theorems

Here we present the actual CoreChaseNode definition and prove some basic properties also relying on the results above.

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

The CoreChaseNode add a couple of fields on top of the RegularChaseNode but the facts field has a different meaning. This is why we duplicate the structure and not jsut extend it. We want to prevent that the CoreChaseNode is accidentally treated as a RegularChaseNode.

• facts : FactSet sig
• origin : Option ((trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length)
• facts_contain_origin_result (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length) : orig ∈ self.origin → orig.fst.val.mapped_head[↑orig.snd].toSet ⊆ self.facts
• core : FactSet sig
• isWeakCore : self.core.isWeakCore
• homSubset : self.core.homSubset self.facts

@[instance_reducible]

instance CoreChaseNode.coreChaseNodeInstance {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} : ChaseNode (CoreChaseNode rules) (RestrictedObsolescence sig) rules

The CoreChaseNode is a ChaseNode where the outgoingFacts are a core of the ingoingFacts.

Equations

• CoreChaseNode.coreChaseNodeInstance = { ingoingFacts := CoreChaseNode.facts, outgoingFacts := CoreChaseNode.core, origin := CoreChaseNode.origin, facts_contain_origin_result := ⋯ }

theorem CoreChaseNode.ingoingFacts_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {node : CoreChaseNode rules} : ChaseNode.ingoingFacts (RestrictedObsolescence sig) rules node = node.facts

theorem CoreChaseNode.outgoingFacts_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {node : CoreChaseNode rules} : ChaseNode.outgoingFacts (RestrictedObsolescence sig) rules node = node.core

theorem CoreChaseNode.out_sub_in {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} : ChaseNode.out_sub_in

The CoreChaseNode has the ChaseNode.out_sub_in property.

theorem CoreChaseNode.equiv_origin_trg_inactive_of_isWeakCore_of_homSubset_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {node : CoreChaseNode rules} {fs : FactSet sig} (wc : fs.isWeakCore) (homSub : fs.homSubset node.facts) (fin : Set.finite fs) (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length) : orig ∈ node.origin → ∀ (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules), orig.fst.equiv trg → ¬trg.val.active fs

Every trigger equivalent to the origin trigger of a CoreChaseNode is inactive for each homSubset of the node's facts, given that this subset is finite.

theorem CoreChaseNode.origin_trg_inactive_of_isWeakCore_of_homSubset_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {node : CoreChaseNode rules} {fs : FactSet sig} (wc : fs.isWeakCore) (homSub : fs.homSubset node.facts) (fin : Set.finite fs) (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length) : orig ∈ node.origin → ¬orig.fst.val.active fs

The origin trigger of a CoreChaseNode is inactive for each homSubset of the node's facts, given that this subset is finite.

theorem CoreChaseNode.equiv_origin_trg_inactive_for_own_core_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {node : CoreChaseNode rules} (fin : Set.finite node.core) (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length) : orig ∈ node.origin → ∀ (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules), orig.fst.equiv trg → ¬trg.val.active node.core

Every trigger equivalent to the origin trigger of a CoreChaseNode is inactive on the node's core.

theorem CoreChaseNode.origin_trg_inactive_for_own_core_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rules : RuleSet sig} {node : CoreChaseNode rules} (fin : Set.finite node.core) (orig : (trg : RTrigger { cond := (RestrictedObsolescence sig).cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length) : orig ∈ node.origin → ¬orig.fst.val.active node.core

The origin trigger of a CoreChaseNode is inactive on the node's core.