A computational framework for institutional agency

Abstract

This paper provides a computational framework, based on defeasible logic, to capture some aspects of institutional agency. Our background is Kanger-Lindahl-Pörn account of organised interaction, which describes this interaction within a multi-modal logical setting. This work focuses in particular on the notions of counts-as link and on those of attempt and of personal and direct action to realise states of affairs. We show how standard defeasible logic (DL) can be extended to represent these concepts: the resulting system preserves some basic properties commonly attributed to them. In addition, the framework enjoys nice computational properties, as it turns out that the extension of any theory can be computed in time linear to the size of the theory itself.

Appendix

1.1 Proofs of the Theorems in Sect. 4

Theorem 1

Let$\#=\Updelta_c, \partial_c, \Upsigma_c, \Updelta_i, \partial_i, \Upsigma_i,$andIbe an institutional action theory. There is no literalpsuch that$I\vdash +\# p$and$I\vdash -\# p$.

Proof

The result is a straightforward consequence of the principle of strong negation [Antoniou et al. 2000a, Antoniou et al. 2000b] used to define the proof conditions for the logic at hand. According to the principle of strong negation the condition for + # is the constructive negation of that of −# and the other way around. Thus if the condition for + # is satisfied the condition for −# fails and the other way around.

Theorem 2

LetIbe an institutional action theory, and$M\in\{c,i\}, i\in A$. $I\vdash +\partial_Mp$and$I\vdash +\partial_M\sim p$iff$I\vdash +\Updelta_Mp$ and $I\vdash +\Updelta_M\sim p.$

Proof

We have to show that if we have both + ∂ _M p and $+\partial_M\neg p$ then the only possible derivation is one where the two are both justified by clause (1) of the proof conditions for + ∂, and combinations of justifications where one of them is justified in terms of clause (2) lead to a contradiction.

It is clear that a combination of clauses (1) does not lead to any contradiction. Thus we have that both + Δ _M p and $+\Updelta_M\neg p$.

Let us consider the cases where one is justified by clause (2). This means that clause (2.1) is satisfied thus for M = c we have $-\Updelta_c {\fancyscript{C}}(p)$, and for M = i both $-\Updelta_i{\fancyscript{C}}(E_ip)$ and $-\Updelta_iE_kp$. But both $\neg p \in {\fancyscript{C}}(p)$ and $\sim p\in{\fancyscript{C}}(E_ip)$, thus we have −Δ _M p. By Theorem 1 it is not possible that both $I\vdash+\Updelta_Mp$ and $I\vdash-\Updelta_Mp$. Thus in this case we get a contradiction.

We examine now the situation where M = c and both conclusions are justified by clause (2). This means that $\exists r^{+}\in R_{sd}[Ep]$ such that the rule is applicable (i.e., the condition of clause (2.2) is satisfied), and at the same time we have that $\exists r^{-}\in R_{sd}[E\sim p]$ such that r ⁻ is applicable. $R_{sd}[E\sim p]\subseteq R[{\fancyscript{C}}(p)]$, thus there must be a rule $t_0\in R[Ep]$ such that t ₀ applicable and $t_0 > r^{-}$ (according to clause (2.3.4)). We have two cases (i) t ₀ is maximal (i.e., $\neg \forall s > t_0$) (ii) t ₀ is not maximal. For (i) we have that $t_0\in R[{\fancyscript{C}}(\sim p)]$ and is applicable thus t ₀ satisfies clauses (2.3) of −∂ _c . Therefore, $-\partial_c\sim p$, and we have a contradiction according to Theorem 1. For (ii) let us consider the set $T_0=\{s: s > t_0\wedge s\in R[E\sim p]\}$. Notice that $r^{-}\notin T_0$, since the theory I is acyclic. From T ₀ we eliminate the rules that are not applicable for condition (2.2) of + ∂ _c , and we call the resulting set S ₀. Since we have + ∂ _c p this means that for every rule s∈S ₀ there is a rule $t^{\prime}\in R[Ep]$ such that the rule is applicable and stronger than s. Let s′ and t ₁ be such rules, If t ₁ is maximal we are done as in the previous reasoning. We build the set $T_1=\{s: s > t_1\wedge s\in R[E\sim p]\}$ and then S ₁ in the same way as S ₀. Since the theory is acyclic we have that $S_0\subset S_1$. We can repeat this construction n times for each rule in S ₀ until we reach a point where the rules we have for Ep are maximal, and we get that $-\partial_c\sim p$, from which we get again a contradiction.

For M = i we have to consider rules in $R^c[{\fancyscript{C}}(E_ip)]\cup R^i[E_kp]\cup R^c[E_kp]$ and the conditions of applicability of clause (2.2) for + ∂ _i , when we build the sets T _n and S _n , but the reasoning for ∂ _i carries over this case as well.

Theorem 3

Let I be an institutional action theory, and $M\in\{c,i\},\,\, i\in A.$

• 1. $\Updelta^{+}_{M} \subseteq \partial^{+}_M \subseteq \Upsigma^{+}_M$;

• 2. $\Upsigma^{-}_M\subseteq \partial^{-}_M \subseteq \Updelta^{-}_M$;

• 3. LetIbe a consistent institutional action theory such that$I\vdash -\Updelta_ip.$If$I\vdash +\partial_iE_jp$then$I\vdash -\partial_ip$.

• 4. For any$i,\,\, \Updelta^{+}_i\subseteq \Updelta^{+}_{c},$and$\partial^{+}_i\subseteq \partial^{+}_c$.

Proof

For 1. The inclusion $\Updelta^{+}\subseteq \partial^{+}$ is immediate given clause (1) of the the proof condition for + ∂ _M , which allows us to extend a derivation with + ∂ _M p if + Δ _M p is already in the derivation.

For the inclusion $\partial^{+}_M\subseteq \Upsigma^{+}_M$, the proof is by induction on the length of the derivation of + ∂ _M p. Notice that it is not possible to have a defeasible derivation consisting of a single step: a minimal defeasible derivation has at least two lines. We will use this case as inductive base. We have two possibilities. We have (i) $P(1)=+\Updelta_Mp$ for p = α, $\alpha\in F$ or $E_ip\in F$, and then $P(2)=+\partial_Mp$ justified by P(1); or (ii) $P(1)=-\Updelta\sim p$ (there are no strict rules for ∼ p), and $P(2)=+\partial_Mp$, justified by the fact that there is a strict or defeasible rule r in $R^M,\,\, A(r)=\emptyset$, and $R[{\fancyscript{C}}(E_ip)]\cup R[E_kp]=\emptyset$ and either $R^c[E_kp]=\emptyset$ or $\forall s\in R^c[E_kp], A(s)\cap\hbox{Lit}=\emptyset$, for $k\neq M$.

For (i) we have that the justification for P(1) corresponds to clause (1) of the proof condition for + Σ _M , thus we can create a proof for + Σ _M p. For (ii) $r\in R_{sd}[p]$ and the conditions (2) and (3) of the proof condition for Σ _M are vacuously satisfied. We can now assume that the property holds for the derivation of + ∂ _M p of length n. For the inductive step we have to consider whether + ∂ _M p is justified by clause (1) or clause (2) of the proof condition for + ∂ _M . For (1) we have two sub-cases: the conclusion is a fact and we can repeat the argument of the inductive base or either clauses (2) or (3) of + Δ _M apply. This means that by inductive hypothesis there is a strict rule that satisfies either the condition of clauses (2) or (3) of Σ _M . In case + ∂ _M p is justified by clause (2.2) of + ∂ _M , then all we have to notice is that we consider the same sets of rules as in clause (2) and (3) of + Σ _M , plus the inductive hypothesis.

For 2. The property follows immediately from 1 and the principle of strong negation.

For 3. To prove this case we have to show how to build a derivation for −∂ _i p given a derivation of $+\partial_iE_kp$, and give the appropriate conditions. If we can derive $+\partial_iE_kp$ since we have $+\Updelta_iE_kp$, then by clause (2.1) we can derive −∂ _i p. Otherwise we consider the rule r used to derive the conclusion. We have two cases (a) $r\in R^i[E_kp]\cup R^c[EE_iE_kp]$ or (b) $r\in R^c[E_kp]$. The two cases are analogous, the only difference is in the condition of applicability of the rule. We will say that r is applicable if the appropriate conditions in clause (2.2) of + ∂ _i are satisfied. We consider two exhaustive cases: (i) r is maximal, i.e., $\neg \exists s, s > r$, (ii) r is not maximal. For (i) the maximality of r ensures that clauses (2.3.1) and (2.3.2) of −∂ _i are satisfied and then the applicability of r makes clause (2.3) true. Thus in this case we can derive −∂ _i p. For (ii) if r is not maximal we consider the set of rules $S_0=\{s: s > r\}$. Let $R^{*}=R^i[p]\cup R^c[EE_ip]\cup R^c[p]$ If $S_0\cap R^{*}=\emptyset$, then clauses (2.3.1) and (2.3.2) are vacuously satisfied and again we are done. Otherwise, consider a rule s∈S ₀. If s is discarded, it meets either conditions of clause (2.3) of + ∂ _i , then we have that s satisfies also either clause (2.2.1) or (2.2.2), and we can remove s from S ₀. Otherwise if s is applicable, then there is a rule t that satisfies (2.3.3), and in particular t > s. At this stage we consider if t is maximal or not. If t is maximal we have a rule that satisfies clause (2.3) of −∂ _i , and again we are done. If t is not maximal, we consider the set $S_1=\{s: s > t\}$. Since >  is acyclic we have that $S_1\cap R^{*}\subset S_0\cap R^{*}$. We can now repeat the above reasoning for the rules in $S_1\cap R^{*}$, and we can repeat it n times for each applicable rule in the set. In this way we remove rules until we arrive at an applicable rule $t^{\prime}\in R^i[p]\cup R^c[E_ip]\cup R^c[p]$ such that it is either maximal or that all stronger rules than it in R ^* are discarded. In this way for every applicable rule in R ^* we have a rule that satisfies clause (2.3) of −∂ _i , and thus we can conclude −∂ _i p.

For 4. The proof is by induction on the length of the proof. We start with definite conclusions. For the inductive base, i.e., $P(1)=+\Updelta_ip$, either $EE_ip\in F$ or there is a rule $r\in R^i_s[p]$ such that $A(r)=\emptyset$. If $EE_ip\in F$, then $E^{\prime}p\in F\,\, (E^{\prime}=EE_i)$ and $R_s^i[p]\subseteq R_s[Ep]$, thus in both cases we can build a derivation for + Δ _c p.

For the inductive step, i.e., $P(n+1)=+\Updelta_ip$, we assume as usual that the property holds up to derivation of length n. Since $R^i_{s}[p]\subseteq R_s[Ep]$, and the conditions of applicability of strict rules in clause (3) of + Δ _i are the same as those of clause (2) of + Δ _c we have the same situation as in the inductive base. If $P(n+1)=+\Updelta_ip$ is justified by clause (4) of + Δ _i (conversion), then there is a rule $r\in R_s^i[p]$ such that $A(r)\cap\hbox{Lit}\neq\emptyset$ and $\forall\alpha\in A(r)$, $+\Updelta_c\alpha\in P(1\ldots n)$, and $\forall a\in A(r), +\Updelta_ia\in P(1\ldots n)$ are under the inductive hypothesis, thus we have that we can build a proof P′ where $\forall a\in A(r), +\Updelta_ca\in P^{\prime}(1\ldots m)$, and thus we can conclude + Δ _c p, using clause (2) of + Δ _c . If $P(n+1)=+\Updelta_ip$ is justified according to clause (2) of + Δ _i , then we have that either $EE_ip\in F$ or there is a rule $r\in R_s[E_ip]$ such that $\forall l\in A(l), +\Updelta l\in P(1\ldots n)$. In both cases we can repeat the reasoning for the inductive base to prove that there is a proof for + Δ _c p.

For ∂⁺ the proof is essentially the same as that for Δ⁺. The only differences are that we have to consider the two clauses (2.3). It is immediate to verify that (2.3.1)–(2.3.3) of + ∂ _c and (2.3) of + ∂ _i are identical; in addition we have that clause (2.3.1) of + ∂ _i (reinstatement by conversion) can be transformed into clause (2.3.4) of + ∂ _c by inductive hypothesis as we did in the case for Δ⁺. Finally, for clause (2.1) all we have to do is to notice that ${\fancyscript{C}}(p)=\{Ep\}$ and ${\fancyscript{C}}(E_ip)=\{E\sim p,E\neg E_{i}p\}$, and thus ${\fancyscript{C}}(p)\subseteq{\fancyscript{C}}(E_ip)$.

Theorem 4

LetIbe an institutional action theory. The extension ofIcan be computer in time linear to the size of the theory, i.e., $O(|R|*|U^I|*|A|).$

Proof

The proof is based on a modification of the algorithm given by Maher [Maher 2001] to show that propositional DL has linear complexity.

The main idea of the proof is to build appropriate data structure to implement a series of transformations reducing the complexity of the rules, and where each literal and modal literal is examined only once. The focal point of the transformations is based on the following properties:

• Let $D\vdash +\partial p$ then $D\cup\{rp_1, \ldots, p_n:p\Rightarrow q\} \equiv D\cup \{r: p_1, \ldots, p_n \Rightarrow q\}.$

• Let $D\vdash -\partial p$ then $D\cup\{r:p_1, \ldots,p_n p\Rightarrow q\}\equiv D$.

The properties allow us (1) to remove already proved literals from the body of rules and (2) to remove rules which have been discarded.

The algorithm has three phases. (1) A pre-processing phase where we use the transformations given in [Antoniou et al. 2001] to transform a theory into an equivalent theory without superiority relation and defeaters; the transformation is linear. (2) A rule loader that parses the theory obtained in the first phase and generates the data structure that encodes the theory. (3) The inference engine applies transformations to the data structure, where at every step it reduces the complexity of the data structure.

We set $V^I=\emptyset$, then the rule loader first scans the set of rules and extracts the set of conclusions Cn(I), and the set of atomic literals in it Lit(I). For each element $l\in Cn(I)\cup Lit(I)$ we add $l,E_il,\neg E_i$ for every i∈A to V ^I if the expressions are well formed according to the formation conditions given in Sect. 3.¹⁰ At this stage the rule loader builds a data structure where every element of V ^I is associated with four hash tables: + h the rules that can prove the elements, + h the rules that can disprove the element, + b the rules that need the element to be applicable, and −b the rules that can be discarded by the element. Each hash table depends on the type of literal it is associated to according to the following conditions.

• For α, we have:

  •  + h is the list of (pointers to) rules in R ^c[α];

  • −h is the list of rules in $R^c[\sim \alpha]$;

  •  + b is the list of rules in $\{r\in R: \alpha\in A(r)\}$;

  • −b is the list of rules in $\{r\in R: \sim \alpha\in A(r)\}$.

• For p (a plain literal), we have:

  •  + h is the list of (pointers to) rules in R[Ep];

  • −h is the list of rules in $R[E\sim p]$;

  •  + b is the list of rules in $\{r\in R: p\in A(r)\}$;

  • −b is the list of rules in $\{r\in R: E\sim p\in A(r)\}$.

• For E _i p (a modalised literal), we have:

  • $+h$ is the list of (pointers to) rules in $R^i[p]\cup R^c[EE_ip]\cup R^c[p]$;

  • −h is the list of rules in $R[E\sim p]\cup R[E\sim E_ip] \cup R^c[E_kp]\cup R^i[E_kp]$ for any k ≠ i;

  •  + b is the list of rules in $\{r\in R: E_ip\in A(r)\}\cup \{r\in R^c: p\in A(r)\}$;

  • −b is the list of rules in $\{r\in R: E\sim p\in A(r)\}\cup \{r\in R:\neg E_ip\in A(r)\}\cup \{r\in R: E_iE_kp\in A(r)\}$, for any k ≠ i.

Each results-in rule r is represented by the rule loader as a pair (h,b) where h is pointer to the head of the rule and b has pointers to the literals in A(r). On the other hand a counts-as rules is implemented as an $n+3\hbox{-tuple}$ (n = |A|, the number of agents in I) $(h,a,b,a_1,\ldots,a_n)$. h is as per results-in rules, a is the set of pointers for action literals in $A(r),\,\, b$ is the set of pointers for non action literals in A(r), and each a _i is either a set of pointers to non action literals if either $A(r)\cap\hbox{Lit}\neq\emptyset$ or there is no literal of the form $E_ip\in A(r)$; otherwise b is the special symbol nil.

The Inference Engine is based on an extension of the Delores algorithm/implementation proposed in [Maher 2001] as a computational model of basic DL. In turn

• 1. It asserts each literal l∈F as a conclusion and removes l from all rules in + b(l), and remove all rules (pointers to rules) in the hash tables for −h. For counts-as rules, if l = α we remove l from the a part of the rules; if l = p, we remove it from the p part of the b part, and if l = E _i m, then (1) we remove both m and E _i m from the rules in + b(E _i p), and (2) for counts-as rules we remove E _i m and m from the b part and p from the a _i part as appropriate.

• 2. Then it scans the set of rules for rules where b is empty. For counts-as rules it looks for rules where both a and either b or a _i are empty for some i∈A. For each of such rules it takes a(r) and E _i a(r) (only E _i a(r) for counts-as rule where a _i is empty), and it checks that −h(a(r)), −h(E _i a(r)) are empty. If so, it adds $a(r),\,\, E_ia(r)$ to the set of conclusions as appropriate.

• 3. It repeats the first step, using the conclusions obtained from the previous step.

• 4. The algorithm terminates when one of the two steps fails. On termination the algorithm outputs the set of conclusions.¹¹

Notice that all the operations described in the above steps correspond to hash functions, thus they have constant complexity O(1). It is immediate to see that the algorithm runs in linear time. Each (modal) atom/literal in a theory is processed exactly once and every time we have to scan the set of rules, thus the complexity of the above algorithm is $O(|V^I|*|R|*|A|)$.