The Backtracking Triggers in the Chase indeed is already part of the Chase #
The goal of this file is to show backtracking_of_loaded_trigger_in_node.
This states that the backtracking of a trigger that is loaded for a chase node
indeed already occurs in that chase node (as intuition suggests).
However, since fresh constants are introduced when backtracking,
this only holds true under the application of a ConstantMapping.
Showing the existence of an appropriate mapping is also part of the theorem.
Furthermore, we require this mapping to map each constant in the mapped body of the trigger and each constant in the rule set to itself.
Intuitively, the mapping shall only remap the constants that where freshly introduced.
theorem
ChaseBranch.backtracking_of_term_in_node
{sig : Signature}
[DecidableEq sig.C]
[DecidableEq sig.V]
[DecidableEq sig.P]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
[GetFreshInhabitant sig.C]
[Inhabited sig.C]
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules)
(term : GroundTerm sig)
(term_mem : term ∈ node.facts.terms)
(forbidden_constants : List sig.C)
:
term.constants ⊆ forbidden_constants →
List.flatMap Rule.constants rl.rules ⊆ forbidden_constants →
∃ (g : ConstantMapping sig), g.apply_fact_set (GroundTerm.backtrackFacts rl term ⋯ ⋯ ⋯ forbidden_constants).fst.toSet ⊆ node.facts ∧ ∀ (d : sig.C), d ∈ forbidden_constants → g d = GroundTerm.const d
theorem
ChaseBranch.backtracking_of_term_list_in_node
{sig : Signature}
[DecidableEq sig.C]
[DecidableEq sig.V]
[DecidableEq sig.P]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
[GetFreshInhabitant sig.C]
[Inhabited sig.C]
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules)
(terms : List (GroundTerm sig))
(terms_mem : terms.toSet ⊆ node.facts.terms)
(forbidden_constants : List sig.C)
:
List.flatMap GroundTerm.constants terms ⊆ forbidden_constants →
List.flatMap Rule.constants rl.rules ⊆ forbidden_constants →
∃ (g : ConstantMapping sig), g.apply_fact_set (GroundTerm.backtrackFacts_list rl terms ⋯ ⋯ ⋯ forbidden_constants).fst.toSet ⊆ node.facts ∧ ∀ (d : sig.C), d ∈ forbidden_constants → g d = GroundTerm.const d
theorem
ChaseBranch.backtracking_of_loaded_trigger_in_node
{sig : Signature}
[DecidableEq sig.C]
[DecidableEq sig.V]
[DecidableEq sig.P]
{obs : ObsoletenessCondition sig}
{kb : KnowledgeBase sig}
[GetFreshInhabitant sig.C]
[Inhabited sig.C]
{cb : ChaseBranch obs kb}
{node : ChaseNode obs kb.rules}
(node_mem : node ∈ cb.toChaseDerivation)
(rl : RuleList sig)
(rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules)
(trg : PreTrigger sig)
(trg_loaded : trg.loaded node.facts)
:
∃ (g : ConstantMapping sig), g.apply_fact_set (PreTrigger.backtrackFacts rl trg ⋯ ⋯ ⋯).fst.toSet ⊆ node.facts ∧ ∀ (d : sig.C),
d ∈ (List.flatMap Fact.constants trg.mapped_body).toSet ∪ kb.rules.constants → g d = GroundTerm.const d