Documentation

ExistentialRules.AlternativeMatches.Basic

Alternative Matches #

Put simply, alternative matches are homomorphisms that witness that a trigger can be satisfied in a way where one of its freshly introduced terms would be redundant. The goal of this notion is to show that a chase without any alternative matches yields a result that is a core, which is, intuitively speaking, the smallest possibly model up to isomorphism.

source
def GroundTermMapping.isAlternativeMatch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (h_alt : GroundTermMapping sig) (trg : PreTrigger sig) (disj_index : Fin trg.mapped_head.length) (fs : FactSet sig) :
Prop

A GroundTermMapping is an alternative match for a head disjunct of a trigger and a given fact set $F$ if (1) the mapping is a homomorphism from the head disjunct into $F$, (2) the mapping is the id on all frontier terms, and (3) there is a term that is freshly introduced by the trigger that does not occur in the mapped version of all fresh terms.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PreTrigger.satisfied_of_alternativeMatch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {fs : FactSet sig} {h_alt : GroundTermMapping sig} {disj_index : Fin trg.mapped_head.length} :
    h_alt.isAlternativeMatch trg disj_index fs → trg.satisfied fs

    If there exists an alternative match for a trigger, then the trigger is satisfied.

    source
    theorem PreTrigger.alternativeMatch_of_satisfied {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {fs : FactSet sig} {disj_index : Fin trg.mapped_head.length} {gt : GroundTerm sig} (gt_in_res_but_not_fs : gt ∈ trg.fresh_terms_for_head_disjunct ↑disj_index ⋯ ∧ ¬gt ∈ fs.terms) :
    trg.satisfied_for_disj fs ⟨↑disj_index, ⋯⟩ → ∃ (h_alt : GroundTermMapping sig), h_alt.isAlternativeMatch trg disj_index fs

    If a trigger is satisfied for a fact set $F$ and there is a term that is freshly introduced by the trigger but does not occur in $F$, then the trigger has an alternative match.