A Query Evaluation Method for ASP with Abduction Ken Satoh National Institute of Informatics, Tokyo, Japan Abstract In this paper, we present a goal-directed proof procedure for ASP with abduction. Our proposed procedure in this paper is correct for any consistent abductive framework proposed in [Kakas90a]. In other words, if the procedure succeeds, there is a set of hypotheses which satisfies a query, and if the procedure finitely fails, there is no such set. If we do not consider abducibles, this procedure is a goal-directed proof procedure for ASP as well. Keywords Logic Programming, Abduction, Topdown Proof Procedure 1. Introduction In this paper, we present a query evaluation method that is correct for every consistent1 abductive framework proposed in [Kakas90a]. If our procedure answers “yes”, then there is a set of hypotheses which satisfies a query. If our procedure answers “no”, then there is no set of hypotheses which satisfies a query. Our procedure can be regarded as a correction of Kakas and Mancarella’s proce- dure [Kakas90b] in the following two points. Forward evaluation of rules: It is important to use integrity constraints to exclude undesirable results from abduction. However, their procedure manipulates a class of integrity constraints in which there is at least one abducible predicate in each integrity constraint. Check for Implicit Deletions: We check consistency for “implicit deletions” first observed by Sadri and Kowalski [Sadri88]. The proposed methods [Kakas90b] do not check consistency of implicit deletion. We believe that this lack of check is a major culprit of incorrectness in these methods. Inversely, we check the implicit deletion in our procedure. For example, consider the following program with an abducible predicate 𝑛𝑜𝑟𝑚𝑎𝑙_𝑏𝑎𝑟𝑏𝑒𝑟† 2 . 2nd Workshop on Goal-directed Execution of Answer Set Programs (GDE’22), August 1, 2022 This paper is an extended abstract of a paper with the title “A Query Evaluation Method for Abductive Logic Programming” that appeared in the Proceedings of the Joint International Conference and Symposium on Logic Programming (JICSLP’92), pp. 671 – 685. " ksatoh@nii.ac.jp (K. Satoh) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings CEUR Workshop Proceedings (CEUR-WS.org) http://ceur-ws.org ISSN 1613-0073 1 Consistency of an abductive framework means that there is a generalized stable model for the framework. 2 ∼ expresses negation as failure 𝑚𝑎𝑛(𝑛𝑜𝑒𝑙) ← (1) 𝑏𝑎𝑟𝑏𝑒𝑟(𝑛𝑜𝑒𝑙) ← (2) 𝑠ℎ𝑎𝑣𝑒𝑠(𝑛𝑜𝑒𝑙, 𝑋) ← 𝑚𝑎𝑛(𝑋), ∼ 𝑠ℎ𝑎𝑣𝑒𝑠(𝑋, 𝑋) (3) 𝑠ℎ𝑎𝑣𝑒𝑠(𝑋, 𝑋) ← 𝑏𝑎𝑟𝑏𝑒𝑟(𝑋), 𝑛𝑜𝑟𝑚𝑎𝑙_𝑏𝑎𝑟𝑏𝑒𝑟† (𝑋) (4) 𝑠ℎ𝑎𝑣𝑒𝑠(𝑐𝑎𝑠𝑎𝑛𝑜𝑣𝑎, 𝑋) ← 𝑏𝑎𝑟𝑏𝑒𝑟(𝑋), ∼ 𝑛𝑜𝑟𝑚𝑎𝑙_𝑏𝑎𝑟𝑏𝑒𝑟 (𝑋) † (5) Since 𝑏𝑎𝑟𝑏𝑒𝑟(𝑛𝑜𝑒𝑙) is true from (2), 𝑠ℎ𝑎𝑣𝑒𝑠(𝑐𝑎𝑠𝑎𝑛𝑜𝑣𝑎, 𝑛𝑜𝑒𝑙) will be derived by using Kakas and Mancarella’s proof procedure and assuming ∼ 𝑛𝑜𝑟𝑚𝑎𝑙_𝑏𝑎𝑟𝑏𝑒𝑟† (𝑛𝑜𝑒𝑙) in (5). However, actually, there is no generalized stable model which satsifies 𝑠ℎ𝑎𝑣𝑒𝑠(𝑐𝑎𝑠𝑎𝑛𝑜𝑣𝑎, 𝑛𝑜𝑒𝑙). We solve this problem by using the above techniques. 2. A Semantics of Abductive Framework We mainly follow the definition of abductive framework in [Kakas90a], but we modify it slightly for notational conveniences. Firstly, we define a rule and an integrity constraint. Definition 1. Let 𝐻 be an atom, and 𝐿1 , ..., 𝐿𝑚 (𝑚 ≥ 0) be literals each of which is an atom or a negated atom of the form ∼𝐵. A rule is of the form: 𝐻 ← 𝐿1 , 𝐿2 , ..., 𝐿𝑚 . We call 𝐻 the head of the rule and 𝐿1 , ..., 𝐿𝑚 the body of the rule. Let 𝑅 be a rule. ℎ𝑒𝑎𝑑(𝑅), 𝑏𝑜𝑑𝑦(𝑅) and 𝑝𝑜𝑠(𝑅) denote the head of 𝑅, the set of literals in the body of 𝑅 and the set of positive literals in 𝑏𝑜𝑑𝑦(𝑅) respectively. Definition 2. Let 𝐿1 , ..., 𝐿𝑚 (𝑚 ≥ 0) be literals. An integrity constraint is of the form: ⊥ ← 𝐿1 , 𝐿2 , ..., 𝐿𝑚 . For a given program (with integrity constraints), we define a stable model (in other words, answer set) as follows. Definition 3. Let 𝑇 be a logic program and Π𝑇 be a set of ground rules obtained by replacing all variables in each rule in 𝑇 by every element of its Herbrand universe. Let 𝑀 be a set of ground atoms from Π𝑇 and Π𝑀 𝑇 be the following (possibly infinite) program. Π𝑀 𝑇 = {𝐻 ← 𝐵1 , ..., 𝐵𝑘 | 𝐻 ← 𝐵1 , ..., 𝐵𝑘 , ∼𝐴1 , ..., ∼𝐴𝑚 ∈ Π𝑇 and 𝐴𝑖 ̸∈ 𝑀 for each 𝑖 = 1, ..., 𝑚.} Let 𝑚𝑖𝑛(Π𝑀𝑇 ) be the least model of Π𝑇 . A stable model for a logic program 𝑇 is 𝑀 iff 𝑀 = 𝑀 𝑚𝑖𝑛(Π𝑀𝑇 ) and ⊥ ̸∈ 𝑀 . This definition gives a stable model of 𝑇 which satisfies all integrity constraints. We say that 𝑇 is consistent if there exists a stable model for 𝑇 . Now, we define an abductive framework. Definition 4. An abductive framework is a pair ⟨𝑇, 𝐴⟩ where 𝐴 is a set of predicate symbols, called abducible predicates and 𝑇 is a set of rules each of whose head is not in 𝐴. We call a set of all ground atoms for predicates in 𝐴 abducibles. As pointed out in [Kakas90a], we can translate a program which includes a definition of abducibles to an equivalent framework that satisfies the above requirement. Moreover, we impose an abductive framework to be range- restricted, that is, any variable in a rule of a program must occur in non-abducible positive literals of the rule. Now, we define a semantics of an abductive framework. Definition 5. Let ⟨𝑇, 𝐴⟩ be an abductive framework and Θ be a set of abducibles. A generalized stable model 𝑀 (Θ) is a stable model of 𝑇 ∪ {𝐻 ← |𝐻 ∈ Θ}. We say that ⟨𝑇, 𝐴⟩ is consistent if there exists a generalized stable model 𝑀 (Θ) for some Θ. 3. Query Evaluation for Abduction Before showing our query evaluation method, we need the following definitions. Let 𝑙 be a literal. Then, 𝑙 denotes the complement of 𝑙3 Definition 6. Let 𝑇 be a logic program. A set of resolvents w.r.t. a ground literal 𝑙 and 𝑇 , 𝑟𝑒𝑠𝑜𝑙𝑣𝑒(𝑙, 𝑇 ) is the following set of rules: 𝑟𝑒𝑠𝑜𝑙𝑣𝑒(𝑙, 𝑇 ) = {(⊥ ← 𝐿1 , ..., 𝐿𝑘 )𝜃| 𝑙 is negative and 𝐻 ← 𝐿1 , ..., 𝐿𝑘 ∈ 𝑇 and 𝑙 = 𝐻𝜃 by a ground substitution 𝜃}∪ {(𝐻 ← 𝐿1 , ..., 𝐿𝑖−1 , 𝐿𝑖+1 , ..., 𝐿𝑘 )𝜃| 𝐻 ← 𝐿1 , ..., 𝐿𝑘 ∈ 𝑇 and 𝑙 = 𝐿𝑖 𝜃 by a ground substitution 𝜃} The first set of resolvents are for negation as failure and the second set of resolvents corresponds with “forward” evaluation of the rule introduced in [Sadri88]. Definition 7. Let 𝑇 be a logic program. A set of deleted rules w.r.t. a ground literal 𝑙 and 𝑇 , 𝑑𝑒𝑙(𝑙, 𝑇 ), is the following set of rules: 𝑑𝑒𝑙(𝑙, 𝑇 ) = {(𝐻 ← 𝐿1 , ..., 𝐿𝑘 )𝜃| 𝐻←𝐿1 , ..., 𝐿𝑘 ∈ 𝑇 and 𝑙 = 𝐿𝑖 𝜃 by a ground substitution 𝜃} Our query evaluation procedure consists of 4 subprocedures, 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, Δ), 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(𝑙, Δ), 𝑟𝑢𝑙𝑒_𝑐𝑜𝑛(𝑅, Δ) and 𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛(𝑅, Δ) where 𝑝 is a non-abducible atom and Δ is a set of ground literals already assumed and 𝑙 is a ground literal and 𝑅 is a rule. 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, Δ) returns a ground substitution for the variables in 𝑝 and a set of ground literals. This set of ground literals is a union of Δ and literals newly assumed during execution of the subprocedure. Other subprocedures return a set of ground literals. The subprocedures have a select operation and a fail operation. The select operation expresses a nondeterministic choice among alternatives. The fail operation expresses immediate termination of an execution with failure. Therefore, a subprocedure succeeds when its inner calls of subprocedures do not encounter fail. We say a subprocedure succeeds with (𝜃 and) Δ when the subprocedure successfully returns (𝜃 and) Δ. The informal specification of the 4 subprocedures is as follows. 3 𝑝 =∼ 𝑝 for a positive literal 𝑝, and ∼𝑝 = 𝑝 for a negative literal ∼𝑝. 1. 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, Δ) searches a rule 𝑅 of 𝑝 in a program 𝑇 whose body can be made true with a ground substitution 𝜃 under a set of assumptions Δ. To show that every literal in the body can be made true, we call 𝑑𝑒𝑟𝑖𝑣𝑒 for non-abducible positive literals in the body. Then, we check the consistency of other literals in the body with 𝑇 and Δ. Note that because of the range-restrictedness, other literals in 𝑅 become ground after all the calls of 𝑑𝑒𝑟𝑖𝑣𝑒 for non-abducible positive literals. 2. 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(𝑙, Δ) checks the consistency of a ground literal 𝑙 with 𝑇 and Δ. To show the consistency for assuming 𝑙, we add 𝑙 to Δ; then, we check the consistency of resolvents and deleted rules w.r.t. 𝑙 and 𝑇 . 3. 𝑟𝑢𝑙𝑒_𝑐𝑜𝑛(𝑅, Δ) checks the consistency of a rule 𝑅 with 𝑇 and Δ. If 𝑅 is not ground, we must check the consistency for ground instances of 𝑅. But it is sufficient to consider every ground instance 𝑅𝜃 in Ω𝑇 ∪{𝑅} . We can prove the consistency by showing that either a literal in 𝑏𝑜𝑑𝑦(𝑅𝜃) can be falsified or 𝑏𝑜𝑑𝑦(𝑅𝜃) can be made true and ℎ𝑒𝑎𝑑(𝑅𝜃) consistent. This procedure can also be used to check integrity for rule addition. 4. 𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛(𝑅, Δ) checks if a deletion of 𝑅 does not cause any contradictions with 𝑇 and Δ. To show the consistency of the implicit deletion of 𝑅, it is sufficient to prove that the head of every ground instance 𝑅𝜃 in Ω𝑇 4 can be made either true or false. Thanks to the range-restrictedness, we can compute all ground instances of a rule 𝑅 (if they are finite) in Ω𝑇 (or Ω𝑇 ∪{𝑅} ). For this, we compute every SLD derivation of a query which consists of all non-abducible positive literals in 𝑏𝑜𝑑𝑦(𝑅) to the abducible-and-negation-removed program 𝑇 − (or (𝑇 ∪ {𝑅})− ). Please see the details of each subprocedure at Figure 1 and Figure 2 in Appendix. In Figure 1, 𝜀 denotes empty substitution and 𝜃𝑖 𝜎𝑖 expresses a composition of two substitutions 𝜃𝑖 and 𝜎𝑖 . Also, we denote a set of non-abducible positive literals, non-abducible negative literals, and abducibles (either negative or positive) in a rule 𝑅 as 𝑝𝑜𝑠(𝑅), 𝑛𝑒𝑔(𝑅) and 𝑎𝑏𝑑(𝑅). If we remove 𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛 and do not consider resolvents obtained with “forward” evaluation of the rule, then this procedure coincides with that of Kakas and Mancarella [Kakas90a]. That is, our procedure is obtained by augmenting their procedure with an integrity constraint checking in a bottom-up manner and with an implicit deletion checking. We can show the following theorems for correctness of successful derivation, consistency check for addition of a rule and finite failure. Theorem 1. Let ⟨𝑇, 𝐴⟩ be a consistent abductive framework. Suppose 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, {}) succeeds with (𝜃, Δ). Then, there exists a generalized stable model 𝑀 (Θ) for 𝑇 such that Θ includes all positive abducibles in Δ and 𝑀 (Θ) |= 𝑝𝜃. This theorem means that if the procedure 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, {}) answers “yes” with (𝜃, Δ), then there is a generalized stable model which satisfies 𝑝𝜃. However, we cannot say in general that we make 𝑝𝜃 true only with positive abducibles in Δ, because there might be some hypotheses which are irrelevant to a query but which we must assume to get consistency. The following theorem states correctness for consistency for addition of a rule. 4 Note that Ω𝑇 ∪{𝑅} = Ω𝑇 since 𝑅 is an instance of a rule in 𝑇 . Theorem 2. Let ⟨𝑇, 𝐴⟩ be a consistent abductive framework. Suppose 𝑟𝑢𝑙𝑒_𝑐𝑜𝑛(𝑅, {}) succeeds, then ⟨𝑇 ∪ 𝑅, 𝐴⟩ is a consistent abductive framework. This means that this procedure can be used to guarantee the existence of a generalized stable model for a given abductive framework ⟨𝑇, 𝐴⟩ if iterative calls of 𝑟𝑢𝑙𝑒_𝑐𝑜𝑛 succeed from ⟨{}, 𝐴⟩ by adding each rule in 𝑇 . The following is a theorem related to correctness for finite failure. Theorem 3. Let ⟨𝑇, 𝐴⟩ be an abductive framework. Suppose that every selection of rules termi- nates for 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, {}) with either success or failure. If there exists a generalized stable model 𝑀 (Θ) for ⟨𝑇, 𝐴⟩ and a ground substitution 𝜃 such that 𝑀 (Θ) |= 𝑝𝜃, then there is a selection of rules such that 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, {}) succeeds with (𝜃, Δ) where Θ includes all positive abducibles in Δ. This theorem means that if we can search exhaustively in selecting the rules and there is a generalized stable model which satisfies a query, then the procedure always answers “yes”. With this theorem, we obtain the following corollary for a finite failure. Corollary 1. Let ⟨𝑇, 𝐴⟩ be an abductive framework. If 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, {}) fails, then for every gener- alized stable model 𝑀 (Θ) for ⟨𝑇, 𝐴⟩ and for every ground substitution 𝜃, 𝑀 (Θ) ̸|= 𝑝𝜃. When the procedure 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, {}) answers “no”, there is no generalized stable model which satisfies the query. Also, this corollary means that we can use a finite failure to check if the negation of a ground literal is true in all generalized stable models since finite failure of 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, {}) means that every generalized stable model satisfies ∼𝑝. 4. Conclusion In this paper, we propose a query evaluation method for an abductive framework. Our procedure can be regarded as an extension of the procedure of Kakas and Mancarella by augmenting forward evaluation of rules and consistency check for implicit deletion. Acknowledgments This work was supported by JSPS KAKENHI Grant Numbers, JP17H06103 and JP19H05470 and JST, AIP Trilateral AI Research, Grant Number JPMJCR20G4. References [Kakas90a] Kakas, A. C., Mancarella, P., Generalized Stable Models: A Semantics for Abduction, Proc. of ECAI’90, pp. 385 – 391 (1990). [Kakas90b] Kakas, A. C., Mancarella, P., On the Relation between Truth Maintenance and Abduction, Proc. of PRICAI’90, pp. 438 – 443 (1990). [Sadri88] Sadri, F., Kowalski, R., A Theorem-Proving Approach to Database Integrity, Founda- tions of Deductive Database and Logic Programming, (J. Minker, Ed.), Morgan Kaufmann Publishers, pp. 313 – 362 (1988). Appendix: Topdown Proof Procedure 𝑑𝑒𝑟𝑖𝑣𝑒(𝑝, Δ) 𝑝: a non-abducible atom; Δ: a set of literals begin if 𝑝 is ground and 𝑝 ∈ Δ then return (𝜀, Δ) elseif 𝑝 is ground and ∼𝑝 ∈ Δ then fail else begin select 𝑅 ∈ 𝑇 s.t. ℎ𝑒𝑎𝑑(𝑅) and 𝑝 are unifiable with an mgu 𝜃 if such a rule is not found then fail Δ0 := Δ, 𝜃0 := 𝜃, 𝐵0 := 𝑝𝑜𝑠(𝑅𝜃), 𝑖 := 0 while 𝐵𝑖 ̸= {} do begin take a literal 𝑙 in 𝐵𝑖 if 𝑑𝑒𝑟𝑖𝑣𝑒(𝑙, Δ𝑖 ) succeeds with (𝜎𝑖 , Δ𝑖+1 ) then 𝜃𝑖+1 := 𝜃𝑖 𝜎𝑖 , 𝐵𝑖+1 := (𝐵𝑖 − {𝑙})𝜎𝑖 , 𝑖 := 𝑖 + 1 and continue end 𝛿 := 𝜃𝑖 for every 𝑙 ∈ 𝑛𝑒𝑔(𝑅𝛿) ∪ 𝑎𝑏𝑑(𝑅𝛿) do begin if 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(𝑙, Δ𝑖 ) succeeds with Δ𝑖+1 then 𝑖 := 𝑖 + 1 and continue end if 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(𝑝𝛿, Δ𝑖 ) succeeds with Δ′ then return (𝛿, Δ′ ) end end (𝑑𝑒𝑟𝑖𝑣𝑒) 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(𝑙, Δ) 𝑙: a ground literal; Δ: a set of literals begin if 𝑙 ∈ Δ then return Δ elseif 𝑙 = ⊥ or 𝑙 ∈ Δ then fail else begin Δ0 := {𝑙} ∪ Δ, 𝑖 := 0 for every 𝑅 ∈ 𝑟𝑒𝑠𝑜𝑙𝑣𝑒(𝑙, 𝑇 ) do if 𝑟𝑢𝑙𝑒_𝑐𝑜𝑛(𝑅, Δ𝑖 ) succeeds with Δ𝑖+1 then 𝑖 := 𝑖 + 1 and continue for every 𝑅 ∈ 𝑑𝑒𝑙(𝑙, 𝑇 ) do if 𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛(𝑅, Δ𝑖 ) succeeds with Δ𝑖+1 then 𝑖 := 𝑖 + 1 and continue end return Δ𝑖 end (𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛) Figure 1: The definition of 𝑑𝑒𝑟𝑖𝑣𝑒 and 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛 𝑟𝑢𝑙𝑒_𝑐𝑜𝑛(𝑅, Δ) 𝑅: a rule; Δ: a set of literals begin Δ0 := Δ, 𝑖 := 0 for every ground rule 𝑅𝜃 ∈ Ω𝑇 ∪{𝑅} do begin select (a) or (b) (a) select 𝑙 ∈ 𝑏𝑜𝑑𝑦(𝑅𝜃) if 𝑙 ∈ 𝑝𝑜𝑠(𝑅𝜃) ∪ 𝑎𝑏𝑑(𝑅𝜃) and 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(𝑙, Δ𝑖 ) succeeds with Δ𝑖+1 then 𝑖 := 𝑖 + 1 and continue elseif 𝑙 ∈ 𝑛𝑒𝑔(𝑅𝜃) and 𝑑𝑒𝑟𝑖𝑣𝑒(𝑙, Δ) succeeds with (𝜀, Δ𝑖+1 ) then 𝑖 := 𝑖 + 1 and continue (b) Δ0𝑖 := Δ𝑖 , 𝑗 := 0 for every 𝑙 ∈ 𝑏𝑜𝑑𝑦(𝑅𝜃) do begin if 𝑙 ∈ 𝑝𝑜𝑠(𝑅𝜃) and 𝑑𝑒𝑟𝑖𝑣𝑒(𝑙, Δ𝑗𝑖 ) succeeds with (𝜀, Δ𝑗+1 𝑖 ) then 𝑗 := 𝑗 + 1 and continue elseif 𝑙 ∈ 𝑛𝑒𝑔(𝑅𝜃) ∪ 𝑎𝑏𝑑(𝑅𝜃) and 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(𝑙, Δ𝑗𝑖 ) succeeds with Δ𝑗+1 𝑖 then 𝑗 := 𝑗 + 1 and continue end if 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(ℎ𝑒𝑎𝑑(𝑅𝜃), Δ𝑗𝑖 ) succeeds with Δ𝑖+1 then 𝑖 := 𝑖 + 1 and continue end return Δ𝑖 end (𝑟𝑢𝑙𝑒_𝑐𝑜𝑛) 𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛(𝑅, Δ) 𝑅: a rule; Δ: a set of literals begin Δ0 := Δ, 𝑖 := 0 for every ground rule 𝑅𝜃 ∈ Ω𝑇 do begin select (a) or (b) (a) if 𝑑𝑒𝑟𝑖𝑣𝑒(ℎ𝑒𝑎𝑑(𝑅𝜃), Δ𝑖 ) succeeds with (𝜀, Δ𝑖+1 ) then 𝑖 := 𝑖 + 1 and continue (b) if 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛(∼ℎ𝑒𝑎𝑑(𝑅𝜃), Δ𝑖 ) succeeds with Δ𝑖+1 then 𝑖 := 𝑖 + 1 and continue end return Δ𝑖 end (𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛) Figure 2: The definition of 𝑟𝑢𝑙𝑒_𝑐𝑜𝑛 and 𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛