Coupling the normative regulation with the constitutive state management in Situated Artificial Institutions

The authors thank the anonymous reviewers of KER for their valuable remarks that have been taken into account in this paper.

In this paper, a substitution is always represented by $\theta$. A substitution is a finite set of pairs $\{\alpha_1/\beta_1,\cdots, \alpha_n/\beta_n\}$ where $\alpha_i$ is a variable and $\beta_i$ is a term. If $\rho$ is a literal, then $\rho\theta$ is the literal resulting from the replacement of each $\alpha_i$ in $\rho$ by the corresponding $\beta_i$. If $P=\{\rho_1,\cdots,\rho_n\}$ is a set of literals, then $P\theta=\{\rho_1\theta,\cdots,\rho_n\theta\}$ (Brachman & Levesque, 2004).

In this paper, sets identified by calligraphic letters (e.g. $\mathcal{N}$) refer to the specification of the system, while sets identified by non-calligraphic letters (e.g. N) refer to the system execution.

In SAI, as in Searle’s work, the expression ‘status function’ means both the status and the corresponding function assigned by the institution to the environmental elements. For example, the agent bob carrying the status function bidder means that bob has both the status and the functions of such status.

The presented formalism employs some elements of the first-order logic language, including (i) constants that refer to elements existing in the modelled world, (ii) variables, (iii) possibly not grounded atomic formulae that represent predicates, and (iv) substitutions of variables (Brachman & Levesque, 2004).

It is beyond the scope of this paper to present in detail the environment. We just consider the elements of $\mathcal{X}$ as existing outside the institution, being available thanks to reliable interfaces.

$\varepsilon$ represents that the element is not present in the constitutive rule. Var, in this paper, represents the whole set of variables that can be used in a constitutive rule. Under a substitution $\theta$, variables $var\in Var$ are substituted by terms.

The symbols $\neg$, $\vee$, and $\wedge$ represent, respectively, negation, disjunction, and conjunction, with the usual semantics of propositional logic.

As events are supposed to be considered at the individual agent level in normative systems (i.e. they can be related to a triggering agent) (De Vos et al., 2013), it is important to record the agent that causes an event-SFA.

Details and comparisons on norms can be found in Boella et al. (2007, 2009), Andrighetto et al. (2013), Alechina et al. (2013), Hollander and Wu (2011), and in the COIN series of workshops (http://www.pcs.usp.br/~coin/), among others.

An implementation of the SAI interpreter for constitutive specifications, normative monitor, interfaces to connect this interpreter to a normative engine based on the model of Panagiotidi et al. (2013) and to the NPL engine, as well as some examples, are available at http://github.com/artificial-institutions/sai.