Unblockability

Here we define what it means for a trigger to be unblockable and we also introduce overapproximations that can be used to witness unblockability.

THIS IS VERY MUCH WORK IN PROGRESS!

Another Condition for Obsolescence

For RPC-like conditions we require another property of ObsolescenceCondition conditions that does not hold for the general definition. The condition shall be stable across certain GroundTermMappings that at least map the head constants to themselves. But this only needs to be true of no fresh term of the trigger already occurs, which, in the context of a chase, means that the trigger itself has not been applied before. The reason for excluding this case is a bit technical. Bottom line, we do this as otherwise the property would simply not hold for SkolemObsolescence. But if a trigger is only obsolete according to SkolemObsolescence because it was already applied, then we do not really care. The interesting case is that a trigger is obsolete because a disjunct without existentials is already present.

Anyway, at the end you probably don't need to care much about the condition. It is enough to show the desired theorems and as a sanity check, we also prove that it holds for both SkolemObsolescence and RestrictedObsolescence as intended.

def ObsolescenceCondition.propagates_under_term_mapping_of_no_fresh_term_occurs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) : Prop

Equations

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

theorem SkolemObsolescence.propagates_under_term_mapping_of_no_fresh_term_occurs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : (SkolemObsolescence sig).propagates_under_term_mapping_of_no_fresh_term_occurs

theorem RestrictedObsolescence.propagates_under_term_mapping_of_no_fresh_term_occurs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : (RestrictedObsolescence sig).propagates_under_term_mapping_of_no_fresh_term_occurs

Unblockability and Overapproximations

We now start to define what it means for a trigger to be unblockable. Also we define the notion of Overapproximation that gives us a way of detecting unblockability. Specific such overapproximations will follow later.

def Trigger.unblockable {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} (rules : RuleSet sig) (hc : HeadChoice sig) (trg : Trigger obs.toLaxObsolescenceCondition) : Prop

A trigger is unblockable for a given HeadChoice if, for every derivation, when the trigger is loaded in a node of the branch indicated by the HeacChoice, then the HeadChoice result of the trigger also occurs in that branch. In the introducing paper this is called g-unblockable.

Equations

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

def FactSet.is_rpc_overapproximation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} (rules : RuleSet sig) (hc : HeadChoice sig) (trg : Trigger obs.toLaxObsolescenceCondition) (fs : FactSet sig) : Prop

This is Definition 7 from the [GC23a] paper.

Equations

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

theorem PreTrigger.unblockable_of_not_obsolete_for_overapproximation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} (obs_propagates : obs.propagates_under_term_mapping_of_no_fresh_term_occurs) {rules : RuleSet sig} {hc : HeadChoice sig} (hc_consistent : hc.consistent_for_equivalent_triggers) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {fs : FactSet sig} : FactSet.is_rpc_overapproximation rules hc trg.val fs → ¬obs.cond trg.val.toPreTrigger fs → Trigger.unblockable rules hc trg.val

This is Lemma 1 from the [GC23a] paper.