Backtracking Facts for a PreTrigger

We mainly lift the machinery around PreGroundTerm.backtrackFacts to PreTrigger. The interesting parts are PreTrigger.backtrackFacts and PreTrigger.backtrackFacts_eq_of_strong_equiv.

def PreTrigger.backtrackTrigger_for_functional_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (trg : PreTrigger sig) (forbidden_constants : List sig.C) (i : Nat) (lt : i < trg.rule.head.length) (v : sig.V) (v_exis : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) : PreTrigger sig

Equations

• trg.backtrackTrigger_for_functional_term forbidden_constants i lt v v_exis = (trg.functional_term_for_var i lt v v_exis).backtrackTrigger ⋯ forbidden_constants

theorem PreTrigger.backtrackTrigger_for_functional_term_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (trg : PreTrigger sig) (forbidden_constants : List sig.C) (i : Nat) (lt : i < trg.rule.head.length) (v : sig.V) (v_exis : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) : (trg.backtrackTrigger_for_functional_term forbidden_constants i lt v v_exis).equiv trg

def PreTrigger.affected_rules_for_backtracking {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : List (Rule sig)

When backtracking a trigger, the "affected" rules are either the rule of the trigger itself or a rule in one of the Skolem terms.

Equations

• trg.affected_rules_for_backtracking = trg.rule :: List.flatMap GroundTerm.rules (List.flatMap GeneralizedAtom.terms trg.mapped_body)

theorem PreTrigger.affected_rules_for_backtracking_eq_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg trg2 : PreTrigger sig) (strong_equiv : trg.strong_equiv trg2) : trg.affected_rules_for_backtracking = trg2.affected_rules_for_backtracking

The affected rules of two PreTriggers are the same if they are strongly equivalent, i.e. they have the same rule and the same mapped body.

def PreTrigger.initial_forbidden_constants_for_backtracking {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : List sig.C

When backtracking a trigger, we forbid the following from being used a fresh constants: all constants that occur in the mapped body or constants in affected_rules_for_backtracking.

Equations

• trg.initial_forbidden_constants_for_backtracking = List.flatMap Fact.constants trg.mapped_body ++ List.flatMap Rule.constants trg.affected_rules_for_backtracking

def PreTrigger.backtrackFacts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (trg : PreTrigger sig) : List (Fact sig) × List sig.C

The backtracking of a PreTrigger consists of its mapped body and the backtrackings of all GroundTerms that occur in its mapped body.

Equations

• One or more equations did not get rendered due to their size.

theorem PreTrigger.backtrackFacts_eq_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (trg trg2 : PreTrigger sig) (strong_equiv : trg.strong_equiv trg2) : trg.backtrackFacts = trg2.backtrackFacts

The backtracking of two PreTriggers is the same if they are strongly equivalent, i.e. they have the same rule and the same mapped body.