# The Ontology for Agents, Systems and Integration of Services: OASIS version
2††thanks: This article is an extended revision of “The Ontology for Agents,
Systems and Integration of Services: recent advancements of OASIS”,
Proceedings of WOA 2022: 23rd Workshop From Objects to Agents, September 1–2,
Genova, Italy. CEUR Workshop Proceedings, ISSN 1613-0073, Vol. 3261,
pp.176–193.

Giampaolo Bella  Domenico Cantone  Carmelo Fabio Longo  Marianna Nicolosi
Asmundo  Daniele Francesco Santamaria Corresponding Author: Daniele Francesco
Santamaria<EMAIL_ADDRESS>Department of Mathematics and Computer
Science, University of Catania, Viale Andrea Doria 6 - 95125 - Catania, Italy

###### Abstract

Semantic representation is a key enabler for several application domains, and
the multi-agent systems realm makes no exception. Among the methods for
semantically representing agents, one has been essentially achieved by taking
a behaviouristic vision, through which one can describe how they operate and
engage with their peers. The approach essentially aims at defining the
operational capabilities of agents through the mental states related with the
achievement of tasks. The OASIS ontology — An Ontology for Agent, Systems, and
Integration of Services, presented in 2019 — pursues the behaviouristic
approach to deliver a semantic representation system and a communication
protocol for agents and their commitments. This paper reports on the main
modeling choices concerning the representation of agents in OASIS 2, the
latest major upgrade of OASIS, and the achievement reached by the ontology
since it was first introduced, in particular in the context of ontologies for
blockchains.

###### keywords:

Semantic Web Ontology OWL Agent Multi-Agent Systems

and

##  1 Introduction

The gist of the _Semantic Web_ [1] is to achieve the full interoperability of
software applications by means of reusing and sharing of data in standard
formats across systems, enterprises, and community boundaries. In the Semantic
Web vision of the Internet, software agents are enabled to query and
manipulate information on behalf of human agents by means of machine-readable
data. Such data carry explicit meaning, expressed with formally defined
semantics through suitable representation languages that support the automatic
processing of information. For this purpose, the _Word Wide Web Consortium_
(W3C) conceived the _Web Ontology Language_ (OWL) [2], a family of knowledge
representation languages relying on Description Logics [3], as a standard for
representing Semantic Web ontologies.111An ontology is a set of
representational primitives, typically classes, attributes and relationships,
defined to formally model a domain of knowledge or discourse. The main
advantage of Semantic Web is to enable users and applications to access data-
oriented web content: users and applications become able to discover and
invoke web resources in a completely automatic way. To capture the complex
interactions of the participants in those environments where people and
organizations dynamically interact with autonomous systems, it is convenient
to identify the proactive stakeholders as autonomous agents [4]. Agents are
defined as entities whose state is perceived as a set of mental components
such as beliefs, capabilities, choices, and commitments [5]. This definition
gives rise to the foundations for the _Agent Oriented Programming_ (AOP)
paradigm, which is most often motivated by the need for open architectures
that continuously evolve to adapt to external changes in a robust, autonomous,
and proactive way. Coherently with this vision, defining suitable
representation mechanisms for agents is still challenging in the large realm
of _Knowledge Representation_.

The authors’ choice for the semantic description of agents focuses on the
agents’ mental states related with their capabilities of reaching an
achievement. Then, the behaviouristic approach, inspired by the _Tropos_
methodology [6], provides a practical and complete operational semantics.
Agent behaviours are decomposed in the atomic and essential mental states of
the agent, in such a way that each single task that the agent seeks to
accomplish is completely described. The _Ontology for Agents, Systems and
Integration of Services_ [7, 8], OASIS in short, applies the behaviouristic
approach to deliver a representation system and a communication protocol for
agents and their commitments. Agents are enabled to manifest the set of
operations that they are able to perform and the type of data required to
execute them. Each output is also identified in a clear, human-understandable
and unambiguous way, in order to abstract from the implementation details and
transparently automate the task of agent discovery. Agents may then join a
collaborative environment in a _plug-and-play_ way, since third-party
interventions are no longer required, thereby profiting from the Semantic Web
features. By means of Semantic Web technologies and of automated reasoners,
data provides machine-understandable information that can be processed,
integrated and exchanged by any type of agent, at a higher level; data
consistency can be easily verified, and information can be inferred and
retrieved through the defined knowledge base. This leads to the realization of
Smart Agents, IA-driven agents that consume information and act with minimal
human intervention. Where required, agents are able to communicate with humans
by using common natural interaction practises, like vocal commands, sentences
transmitted via texts or gestures.

This article revises a previous workshop paper [8] by reporting on the full
modeling choices behind the latest version of OASIS, named OASIS 2\. In brief,
the new ontology reviews the representation of agents and their commitments
and also introduces the constitutional elements that make it a valid means for
defining a _Semantic Blockchain_. The full OASIS 2 is available online [9].

The paper is organized as follows. Section 2 introduces the main features of
OASIS 2 and how it models agent behaviours and commitments. Section 3 reports
on the contributions given by OASIS, depicting the main differences between
OASIS and OASIS 2\. Section 4 presents related works discussing similarities
and differences with OASIS 2, while Section 5 concludes the paper with future
perspectives.

##  2 The OASIS 2 ontology

This section is devoted to the OASIS 2 modeling approach for representing
agents and their commitments. OASIS 2 is a foundational OWL 2 ontology that
leverages the behaviouristic approach derived from the _Theory of Agents_ and
the related mentalistic notions to represent multi-agent systems. The approach
aims at describing how agents behave with respect to the environment by
representing their essential mental states, namely _behaviours_ , _goals_ ,
and _tasks_. Behaviours represent the mental state of the agent associated
with its capability of activating, modifying the environment or doing
something; goals describe mental attitudes representing preferred progressions
of a particular system that the agent has chosen to put effort into bringing
about [10]; tasks depict how such progressions are carried on and describe
atomic operations that agents may perform.

Such behaviouristic approach is an effective way for semantically describing
agents by characterizing their capabilities. Agents are enabled to report the
set of activities that they are able to perform, the types of data required to
execute those activities as well as the expected output through the
description of their behaviours. Agents’ implementation details are abstracted
away so as to make the discovery of agents transparent, automatic, and
independent of the underlying technical infrastructure. As a consequence,
agent commitments are clearly described and the entire evolution of the
environment is unambiguously represented, searchable, and accessible: agents
may join a collaborative environment in a plug-and-play fashion, as there is
no more need of third-party interventions. The behaviouristic approach is
exploited by OASIS 2 to characterize agents in terms of the actions they are
able to perform, including purposes, goals, responsibilities, information
about the world they observe and maintain, and their internal and external
interactions. Finally, OASIS 2 models the executions and assignments of tasks,
restrictions, and constraints used to establish agent responsibilities and
authorizations.

In OASIS 2, agents and their interactions are represented by carrying out
three main steps, namely a) an optional step that consists in modeling general
abstract behaviours (called _templates_) from which concrete agent behaviours
are drawn, b) modeling concrete agent behaviours, possibly, drawn by agent
templates, and c) modeling actions and associating them with the corresponding
behaviours.

The first step, not mandatory, consists in defining the agent’s behaviour
template, namely a higher-level description of the behaviour of abstract
agents that can be implemented to define more specific and concrete behaviours
of real agents; for example, a template may be designed to describe which
features a trader agent should own. Moreover, templates are useful to guide
developers in the definition of the behaviours of their specific agents. To
describe abstract agent’s capabilities to perform actions, an agent template
comprises three main elements, namely behaviour, goal, and task. In fact, the
core of the agent representation mechanism in OASIS 2 revolves around the
description of atomic operations introduced by the definition of tasks, i.e.,
the most simple (atomic) operations that agents are able to actually perform
including, possibly, input and output parameters required to accomplish them.

The second step consists in representing concrete agent behaviours either by
specifying a shared template or by defining it from scratch. In both cases,
concrete behaviours are modeled analogously to those of templates, where the
models of ideal features are replaced with actual characteristics. Behaviours
drawn by shared templates are clearly associated with them in order to depict
the behaviour inheritance relationship.

In the last step, actions performed by agents are described as direct
consequences of some behaviours, and are associated with the behaviours of the
agent that performed them. To describe such an association, OASIS 2 introduces
_plan executions_. Plan executions describe the actions performed by an agent
and associated with one of its behaviours. Associations are carried out by
connecting the description of the performed action to the behaviour from which
the action has been drawn: actions are hence described by suitable graphs that
retrace the model of the agent’s behaviour. Additionally, plans can be either
submitted to agents as request of performing some actions or they can be
assigned by specific agents called _entruster agents_.

In OASIS 2, agent templates are defined according to the UML diagram in Fig.
1.

Figure 1: UML diagram of agent templates in OASIS 2

To describe how both abstract and concrete agents perform actions, the
description of agents comprises three main elements, namely _behaviour_ ,
_goal_ , and _task_. Agent tasks, in their turn, describe atomic operations
that agents may perform, including possibly input and output parameters
required to accomplish them. Those elements in OASIS 2 are introduced by way
of the following classes:

  * •

Agent: this class comprises all the individuals representing agents. Instances
of such a class are connected with one or more instances of the class
Behaviour by means of the OWL object-property hasBehaviour.

  * •

Behaviour: behaviours can be seen as collectors comprising all the goals that
an agent can achieve. Instances of Behaviour are connected with one or more
instances of the class GoalDescription by means of the object-property
consistsOfGoalDescription.

  * •

GoalDescription: goals represent containers embedding all the tasks that the
agent can achieve. Instances of GoalDescription comprised by a behaviour may
also satisfy dependency relationships introduced by the object-property
dependsOn. Goals are connected with the tasks that form them and are
represented by instances of the class TaskDescription through the object-
property consistsOfTaskDescription.

  * •

TaskDescription: this class describes atomic operations that agents perform.
Atomic operations are the most simple actions that agents are able to execute
and, hence, they represent what agents can do within the environment. Atomic
operations may depend on other atomic operations when the object-property
dependsOn is specified. Atomic operations whose dependencies are not
explicitly expressed are intended to be performed in any order.

The core of agent behaviour revolves around the description of atomic
operations represented by instances of the class TaskDescription that
characterizes the mental state corresponding to commitments. In their turn,
instances of the class TaskDescription are related with the following five
elements that identify the operation:

  * •

An instance of the class TaskOperator, characterizing the mental state
corresponding to the action to be performed. Instances of TaskOperator are
connected either by means of the object-property refersExactlyTo or
refersAsNewTo to instances of the class Action. The latter class describes
physical actions represented by means of entity names in the form of infinite
verbs (e.g., produce, sell). Specifically, the object-property refersExactlyTo
is used to connect the task operator with a precise action having a specific
IRI, whereas refersAsNewTo is used to connect a task operator with an entity
representing an action of which only a general abstract description is given
(for example, an action for which only the type is known).

In the latter case, the action is also defined as an instance of the
TemplateThing: such instances are used to introduce entities that represent
templates for the referred element describing the characteristics that it
should satisfy. To specify the classes that the entity must be instances of,
it is possible to connect the entity with instances of the desired classes
using the object-property refersAsInstanceOf. Finally, TemplateThing is a
novel OASIS 2 class, used to characterize all the individuals involved in the
definition of behaviour templates and to distinguish them from the entities
representing concrete behaviours, plans or actions, thus eliminating the need
of having separated models for those aspects.

  * •

Possibly, an instance of the class TaskOperatorArgument, connected by means of
the object-property hasTaskOperatorArgument and representing additional
specifications or subordinate characteristics of task operators (e.g., on,
off, left, right). Instances of TaskOperatorArgument are referred to the
operator argument by using either the object-property refersAsNewTo or
refersExactlyTo.

  * •

An instance of the class TaskObject, connected by means of the object-property
hasTaskObject and representing the template of the object recipient of the
action performed by the agent (e.g., price). Instances of TaskObject are
referred to the action recipient by specifying either the object-property
refersAsNewTo or refersExactlyTo.

  * •

Input parameters and output parameters are introduced by instances of the
classes TaskInputParameter and TaskOutputParameter, respectively. Instances of
TaskDescription are related with instances of the classes TaskInputParameter
and TaskOutputParameter by means of the object-properties
hasTaskInputParameter and hasTaskOutputParameter, respectively. Instances of
TaskInputParameter and of TaskOutputParameter are referred to the parameter by
specifying either the object-property refersAsNewTo or refersExactlyTo.
Moreover, the classes TaskInputParameter and TaskOutputParameter are also
subclasses of TaskParameter.

Finally, in the case of agent behaviour templates, instances of Agent,
Behaviour, GoalDescription, TaskDescription, TaskOperator,
TaskOperatorArgument, TaskObject TaskInputParameter, and TaskOutputParameter
are also instances of TemplateThing.

Figure 2: Example of an OASIS 2 agent template

Fig. 2 illustrates an example of an agent template describing the procedure of
smart contracts for minting ERC-721 compliant non-fungible tokens (NFTs) on
the Ethereum blockchain. The agent template described in the example comprises
a single behaviour, constituted by a single goal that in its turn comprises a
single task. The task, which represents the ability of the agent to mint a
NFT, provides four elements:

  * •

mint_ERC721_token_task_operator, representing the mental state of the
behaviour’s action (the task operator), which is associated with the
individual mint, the latter describing the capability of generating a coin;

  * •

mint_ERC721_token _task_operator_argument, introducing an additional feature
(the operator argument) associated with the action and represented by the
individual blockchain_digital_token. It describes the fact that the minting
action is referred to a digital coin on the blockchain. Task operator and its
argument describe together the capability of minting tokens on the blockchain;

  * •

mint_ERC721_token_task_object, representing the recipient of the operation,
which is related with an instance of the class EthereumTokenERC721 by means of
the object-property refersAsNewTo. Such an instance comprises all the features
that the recipient of the minting action should own, that is being a ERC-721
token. In fact, the concrete actions implementing the behaviour template for
minting tokens are supposed to generate ERC-721 compliant tokens that
therefore can provide additional properties, as for example the description of
specific physical assets;

  * •

_mint_ERC721_token_task_output_ , representing the output of the operation,
namely the same token recipient of the _mint_ action.

In the second step, concrete agent behaviours are defined either by
instantiating one or more templates or from scratch. In OASIS 2, the modeling
pattern of concrete behaviours has a structure analogous to the one of
behaviour templates, illustrated above, with the difference that individuals
used to define a concrete behaviour are instances of the class BehaviourThing
(instead of instances of the class TemplateThing).

An example of concrete behaviour is illustrated in Fig. 3.222The smart
contract is freely inspired from the one released by the Sicilian Wheat Bank
(SWB) S.p.A. The figure depicts a concrete behaviour for minting ERC-721
tokens, devised from the template in Fig. 2. The template is implemented by
the concrete behaviour that provides a graph similar to the template’s one,
where the instances of TemplateThing are replaced with instances of
BehaviourThing. The entity connected with the task object and the output
parameter remain the same both in the template and in the concrete behaviour
so as to establish that recipients of the concrete behaviours are objects of
type EthereumTokenERC721 or of one of its subclasses.

Figure 3: Example of OASIS 2 concrete behaviour

Concrete behaviours can be connected with the template they are drawn from. In
order to describe the fact that concrete agents inherit their behaviours from
a common shared template, the instances related with the concrete behaviours
are connected with the instances of the template through the sub-properties of
the object-property overloads. The association is carried out by connecting
the instances of the classes:

  * •

Behaviour, by means of overloadsBehaviour;

  * •

GoalDescription, by means of overloadsGoalDescription;

  * •

TaskDescription, by means of overloadsTaskDescription;

  * •

TaskObject, by means of overloadsTaskObject;

  * •

TaskOperator, by means of overloadsTaskOperator;

  * •

TaskInputParameter, by means of overloadsTaskInputParameter;

  * •

TaskOutputParameter, by means of the object-property
overloadsTaskOutputParameter.

As a last step, agent commitments devised from behaviours are introduced to
describe agent actions. In OASIS 2, commitments are represented by adopting
the same pattern presented for abstract behaviours with the difference that i)
instances of the class TemplateThing are instead modeled as instances of the
class ExecutionThing and ii) the agent responsible for the execution of the
action is related with the plan representing the commitment by means of the
object-property performsPlanExecution, subproperty of performs. The class
ExecutionThing is introduced to characterize all the entities involved in the
definition of concrete actions and to distinguish them from the ones
introduced for templates, behaviours, and plans. For instance, Fig. 4 depicts
the action of minting the token number 32 committed by the smart contract
whose behaviour is illustrated in Fig. 3. In the example, suitable instances
of ExecutionThing that represent the commitment stages take the place of the
instances of BehaviourThing, introduced in the concrete behaviour. Moreover,
the template representing general Ethereum tokens has been replaced with an
instance representing the token number 32, namely SWB_token32.

Figure 4: Example of OASIS 2 agent’s commitment Figure 5: UML diagram of agent
plans in OASIS 2

In order to relate agent commitments with the behaviour from which they are
drawn, subproperties of the object-property drawnBy are introduced.
Specifically, planExecutionDrawnBy connects the instance of GoalDescription of
the agent action to its analogue of agent behaviour; much in the same way,
goalExecutionDrawnBy connects the instance of the class GoalDescription of the
commitment with its analogue, while taskExecutionDrawnBy, taskObjectDrawnBy,
taskOperatorDrawnBy, taskInputParameterDrawnBy, and taskOutputParameterDrawnBy
are introduced for TaskDescription, TaskObject, TaskOperator,
TaskInputParameter, and TaskOutputParameter, respectively.

Agents that desire to engage peers with performing actions can submit _plans_
, namely descriptions of actions that they wish to be realized. For plans, a
model analogous to the one describing behaviours have been introduced, where
instances of BehaviourThing are replaced with instances of PlanningThing and
agents proposing plans are connected with the instances of PlanningThing and
Behaviour of the plan by means of the object-property requestsPlan (see Fig.
5). The class PlanningThing is introduced to characterise all the individuals
involved in the definition of plans and to distinguish them from the ones
introduced for representing templates, behaviours, and actions.

Usually, agents proposing plans identify the behaviours responsible for their
realization beforehand, in such a way as to completely describe and trace how
agent intentions are realized. In this case, the entities representing the
submitted plan are related with the entities describing the responsible
behaviour by means of suitable subproperties of the object-property
submittedTo, relating instances of PlanningThing with instances of
BehaviourThing as follows: a) planDescriptionSubmittedTo, for instances of
Behaviour; b) goalDescriptionSubmittedTo, for instances of GoalDescription; c)
taskDescriptionSubmittedTo, for instances of TaskDescription, d)
taskObjectSubmittedTo, for instances of TaskObject; e)
taskOperatorSubmittedTo, for instances of TaskOperator; f)
taskInputParameterSubmittedTo, for instances of TaskInputParameter; and g)
taskOutputParameterSubmittedTo, for instances of TaskOutputParameter.

In a similar way, plans are also related with the agent’s action realizing
them. For this purpose, the subproperties of the object-property hasExecution
are introduced, namely hasPlanExecution, hasGoalExecution, hasTaskExecution,
hasTaskObjectExecution, hasTaskOperatorExecution,
hasTaskInputParameterExecution, and hasTaskOutputParameterExecution.

Figure 6: UML diagram of agent entrustments in OASIS 2

In OASIS 2, agents can assign plans to agent peers that can perform them by
means of _entrustments_. Entrustments represent the capability of _entruster
agents_ to engage a _performer agent_ so that it executes a given plan
submitted by a _requester agent_ (for example, a domotic assistant that
activates an IoT device on behalf of a human agent). The association among the
behaviours of entruster, requester, and performer are illustrated in Fig. 6.
The entrustment is introduced by means of a graph that retraces the structure
of that of agent behaviours, where instances of BehaviourThing are replaced
with instances of EntrustmentThing. In order to associate a plan with the
behaviour of the agent chosen to perform it, the elements of the entrustment
are connected to a) the related elements of the plan, by means of the
subproperties of entrustedBy, and to b) the related elements of the behaviour
of the performer agent, by means of the subproperties of entrustedFrom. More
precisely, entrustedBy provides the object-properties a) planEntrustedBy, to
connect the entrustment to the requested plan; b) goalEntrustedBy, to connect
the entrustment’s goal to the plan’s goal; c) taskEntrustedBy, to connect the
entrustment’s task to the plan’s task; d) taskObjectEntrustedBy, to connect
the entrustment’s task object to the plan’s task object; e)
taskOperatorEntrustedBy, to connect the entrustment’s task operator to the
plan’s task operator; f) taskOperatorArgumentEntrustedBy, to connect the
entrustment’s task operator argument to the plan’s task operator argument; g)
taskInputParameterEntrustedBy, to connect the entrustment’s task input
parameter to the plan’s input parameter; and h)
taskOutputParameterEntrustedBy, to connect the entrustment’s task output
parameter to the plan’s task output parameter. On the other hand,
entrustedFrom provides analogous subproperties to connect each element of the
entrustment to the related ones of the performer agents.

A single plan entrustment may be constituted by more than one goal
entrustment, which in its turn may be constituted by one or more task
entrustments, depending on how the requested plan is structured. In case that
the requested plan is constituted by two or more tasks, each task can be
entrusted to different agent behaviours, thus ensuring the representation of
cooperative systems, where the effort of solving plans is distributed among
participants. Finally, when the performer agent executes the entrusted plan, a
plan execution is introduced as described above. As a consequence, the plan
entrustment is associated with the plan execution by connecting the elements
of the plan entrustment to the related elements of the plan execution through
the subproperties of entrustedWith in an analogous way to entrustedBy and
entrustedFrom. Additionally, the task of the plan entrustment is associated
with the performer agent by means of the object-property entrusts.

##  3 OASIS so far

The first version of OASIS was presented in [7], together with the
architecture design and implementation of a domotic assistant based on it,
called Prof-Onto.333The latest version of Prof-Onto is called Clara [11].  Our
approach represents a first foundational contribution to the adoption of
Semantic Web technologies for defining a transparent communication protocol
among agents. The proposed protocol was based on the exchange of RDF-based
fragments of OASIS, each consisting of a description of a request to be
fulfilled, by means of suitably constructed queries, against the description
of the agent’s behaviour selected to satisfy it.

In [12], the OASIS ontology is extended with _Ontological Smart Contracts_ (in
short, OSCs) and conditionals. OSCs are intended as agreements among agents
expressed through suitable ontological fragments that permit to establish
responsibilities and authorizations among agents. Conditionals have many
purposes, namely they are used a) to restrict and limit agent interactions, b)
to define activation mechanisms that trigger agent actions, and c) to define
constraints and contract terms on OSCs.

Additionally, OSCs can be secured through digital decentralized public ledgers
such as the blockchain. For this purpose, [12] also sketches the architecture
of a framework based on the _Ethereum_ blockchain and the _Interplanetary File
System_. The framework leverages a suitable Ethereum smart contract to claim
and transfer non-fungible tokens (NFT) compliant with the Ethereum ERC-721
standard, representing the ownership of OWL ontological fragments stored on
the IPFS. Moreover, smart contracts allow one to verify unauthorized
modifications both on the hierarchy of imported ontologies and on the SPARQL
queries defined to verify the OSCs. The work also represents a first approach
towards the definition of a _Semantic Blockchain_ , where operations over
smart contracts are semantically represented. For this purpose, in [13], the
definition of digital contracts is extended over the blockchain to include
smart contracts, intended as programs running on the blockchain and
interpreted as digital agents in an OASIS fashion, including their operational
semantics and tokens exchanged through them. It also advances the first
approach to formalize ERC-721 compliant smart contracts through Semantic Web
ontologies by leveraging, in turn, the behaviouristic approach pursued by
OASIS. The main capabilities of ERC-721 compliant smart contracts are
represented and exploited to fully enable a _Semantic Blockchain_ that
provides agents and humans with means for probing the Ethereum blockchain,
thus discovering smart contracts and their interactions, transactions,
exchanges of cryptocurrencies and tokens, on the one hand, and for building
oracles for distributed ledgers, on the other. The proposed approach is part
of the POC4COMMERCE project [14] funded by the NGI-ONTOCHAIN consortium [15].
POC4COMMERCE, which leverages OASIS as foundational ontology, is presented in
[16], while its design and analysis can be found in [17] and in [18]. In the
context of the POC4COMMERCE project, a semantic search engine harnessing the
expressive power of OASIS for the e-commerce realm is under development,
currently standing at TRL3 (Technology Readiness Level 3).

Recently, an extension of OASIS towards OASIS 2 as described below has been
presented in [8].

OASIS 2 enhances OASIS thanks to a substantial refactoring to re-shape
behaviours, plans and actions. In OASIS, behaviour templates, behaviours,
plans, and actions are introduced by four distinct graphs rooted in the
classes BehaviourTemplate, Behaviour, Plan and PlanExecution, respectively
(see [7] for the UMLs). Instead, OASIS 2 introduces the novel classes
TemplateThing, BehaviourThing, PlanningThing, and ExecutionThing to
characterize the individuals defining behaviour templates, behaviours, plans,
and actions, respectively. For the four mentioned aspects of agents, OASIS 2
adopts the same graph involving the classes Behaviour, GoalDescription, and
TaskDescription. As a consequence, the classes TaskFormalInputParameter and
TaskFormalOutputParameter used to define parameters of behaviours in OASIS are
replaced by the classes TaskInputParameter and TaskOutputParameter, adopted in
combination with the class BehaviourThing, while the classes
TaskActualInputParameter and TaskActualOutputParameter used to define
parameters of agent actions are replaced by the classes TaskInputParameter and
TaskOutputParameter, used in combination with the class ExecutionThing.
Concerning agent templates, the input and output parameters are introduced by
way of the classes TaskInputParameter and TaskOutputParameter, respectively,
in combination with the class TemplateThing. Finally, the object-properties
connecting the agent mental states (namely, consistsOfGoalDescription,
consistsOfTaskDescription, hasTaskInputParameter and hasTaskOutputParameter)
have been unified, thus removing the idiosyncrasy resulting from representing
strictly correlated aspects (i.e., abstract behaviour, concrete behaviour,
action, and plan) through distinct models.

Additionally, the new approach proposed by OASIS 2 streamlines the
representation of agents, also clarifying their relationships and
interactions, thus bringing coherence to the model and making it more compact,
smooth, and consistent. Incidentally, the novel model supports the definition
of more efficient and simple queries. Most importantly, OASIS 2 introduces the
assignment of plans and, at the same time, models the constitutional elements
of blockchains, which were missing in OASIS.

##  4 Related Work

The integration of agent systems and the Semantic Web has been investigated in
several contexts [19, 20, 21] and the advantages of ontology-based
applications have been recognized in the realm of MAS [22]. Ontologies for MAS
have been modeled by taking approaches similar to those of _Agent-Oriented
Software Engineering_ (AOSE) [23], a software engineering paradigm for the
development of complex MAS based on the abstraction of agent roles and on
their organizations. In [24], an ontology for agent-oriented software
engineering is proposed together with a tool that uses the ontology to
generate programming code for MAS. The two approaches do not examine agents
and their interactions in detail and do not take into account an appropriate
modeling of agent communication, which, by contrast OASIS does since its
inception thanks to a protocol based on the exchange of suitable RDF
fragments.

Some results attempt to bring uniformity and coherence to the increasing
volume and diversity of information in a specific domain, but domain-legacy
generally makes them not applicable to other contexts even if they provide
interesting insights for a general approach. The downside of those models lies
in the absence of relationships between agents and their commitments, which
instead represents the core of agent-oriented representations. That implies
the inability of finding agents/services with specific capabilities, invoking
them, and enabling their interoperability, which, by contrast is smooth in
OASIS.

The authors of [25] propose an ontology-based framework for seamlessly
integrating agents and Semantic Web Services, focusing on biomedical
information, while an infrastructure to allow agent-oriented platforms to
access and query domain-specific OWL ontologies is presented in [26]. An
approach to design scalable and flexible agent-based manufacturing systems
integrating automated planning with multi-agent oriented programming for the
_Web of Things_ (WoT) is introduced in [27]. Concerning the _Internet of
Things_ (IoT), ontological approaches mainly focus on the description of
sensors, with the purpose of collecting data associated with them for
generating perceptions and abstractions of the observed world [28]. A
comprehensive ontology for representing IoT services is presented in [29]
together with a discussion on how it can be used to support tasks such as
service discovery, testing, and dynamic composition, taking into account also
parameters such as _Quality of Services_ (QoS), _Quality of Information_
(QoI), and IoT service tests. A unified semantic knowledge base for the
Internet of Things (IoT) is proposed in [30], capturing the complete dynamics
of IoT entities, as for instance enabling semantic searching while hiding
their heterogeneity. All these works are valuable and have influenced the
gestation of OASIS. In consequence, our ontology is most general, offering an
extensive range of constitutional elements to represent virtually any domain
that is amenable to a behaviouristic formalisation, including web services,
Web of Things (WoT), IoT, and quality evaluation.

In the realm of WoT, the W3C advances a formal model and a common
representation for WoT descriptions based on a small vocabulary that makes it
possible both to integrate diverse devices and to allow diverse applications
to interoperate [31]. The representation system provides a way to expose the
state of an object and to invoke functions that, however, must be known in
advance. This may complicate the task of invoking agents that would like to
join the environment in a plug-and-play manner. Moreover, the provided schema
does not fully allow agents to interact according to the specific roles they
aim to play. This is clearly possible in OASIS.

Worthy to be mentioned, conjoining the blockchain with ontologies [32, 33] is
a recent research area, mainly focused in developing a characterization of
blockchain concepts and technologies through Semantic Web but without a
precise analysis of the operational semantics of smart-contracts. In [34], a
theoretical contribution looking at the blockchain through an ontological
approach has been provided. In [35], the authors propose a blockchain
framework for SWoT contexts settled as a _Service-Oriented Architecture_
(SOA), where nodes can exploit smart contracts for registration, discovery,
and selection of annotated services and resources. Other works aim at
representing ontologies within a blockchain context. For instance, in [36]
ontologies are used as a common data format for blockchain-based applications
such as the proposed provenance traceability ontology, but are limited to
describe implementation aspects of the blockchain. Therefore, the semantic
description of smart contracts and their actions is missing from the
literature, and this is one of the major results brought by OASIS through its
formalisation of smart contracts conceived as agents modeled according to the
approach pursued by the behaviouristic vision.

##  5 Conclusions

This paper presented the epistemological choices of the latest release, OASIS
2, of _Ontology for Agents, Systems and Integration of Services_. OASIS 2 is a
foundational ontology that takes the behaviouristic approach from the _Theory
of Agents_ and inherits the related mentalistic notions to represent agents.
The paper focused on how OASIS 2 represents agent templates, concrete agents,
agent commitments, plans, and entrustments (underlining the differences with
respect to the previous version). It also introduced the representation of
plan entrustments, a new feature of OASIS 2, and illustrated the main
contributions of OASIS 2 and how it evolved since its first release, in
particular as a consequence of its adoption in the realm of ontologies for
blockchains. In fact, the NGI-ONTOCHAIN consortium aimed at delivering the
ontological foundation of a blockchain-oriented e-commerce by adopting OASIS 2
and its behaviouristic approach.

Many advancements of OASIS 2 are in progress. Representing how agents reach
consensus is one of the future challenges, together with the modeling of their
behaviours. We shall also consider how to model in OASIS 2 agent roles,
modular behaviours, and processes. In addition, we intend to apply agent
conditionals to represent security constraints for cybersecurity threat
contexts, in particular for the purpose of semantically representing
authentication and confidentiality properties for agents. We shall consider
how to integrate OASIS 2 with the main frameworks such as JADE [37] to
automatically generate agents and artifacts, and how it can be exploited by
_CArtAgO_ [38], a framework for building shared computational worlds.

## References

  * [1] T. Berners-Lee, J. Hendler and O. Lassila, The Semantic Web, Scientific American 284(5) (2001), 34–43. http://www.sciam.com/article.cfm?articleID=00048144-10D2-1C70-84A9809EC588EF21.
  * [2] P. Hitzler, M. Krötzsch, B. Parsia, P.F. Patel-Schneider and S. Rudolph, OWL 2 Web Ontology Language Primer, W3C Recommendation, World Wide Web Consortium, 2009\. http://www.w3.org/TR/owl2-primer/.
  * [3] F. Baader, I. Horrocks, C. Lutz and U. Sattler, An Introduction to Description Logic, Cambridge University Press, 2017\.
  * [4] N.R. Jennings and M.J. Wooldridge (eds), Agent Technology: Foundations, Applications, and Markets, Springer-Verlag, Berlin, Heidelberg, 1998\. ISBN ISBN 3540635912.
  * [5] Y. Shoham, Agent-oriented Programming, Artificial Intelligence 60(1) (1993), 51–92.
  * [6] P. Bresciani, A. Perini, P. Giorgini, F. Giunchiglia and J. Mylopoulos, Tropos: An Agent-Oriented Software Development Methodology, in: Autonomous Agents Multi Agent Systems, Vol. 8:3, 2004, pp. 203–236.
  * [7] D. Cantone, C.F. Longo, M. Nicolosi-Asmundo, D.F. Santamaria and C. Santoro, Towards an Ontology-Based Framework for a Behavior-Oriented Integration of the IoT, in: Proceedings of the 20th Workshop From Objects to Agents, 26-28 June, 2019, Parma, Italy, CEUR Workshop Proceeding Vol. 2404, 2019, pp. 119–126.
  * [8] G. Bella, D. Cantone, M. Nicolosi-Asmundo and D.F. Santamaria, The Ontology for Agents, Systems and Integration of Services: recent advancements of OASIS, in: Proceedings of WOA 2022- 23nd Workshop From Objects to Agents, 1–2, September 2022, Genova, Italy, CEUR Workshop Proceedings ISSN 1613-0073, Vol. 3261, 2022, pp. 176–193.
  * [9] G. Bella, D. Cantone, M. Nicolosi-Asmundo and D.F. Santamaria, OASIS 2, 2022\. https://www.dmi.unict.it/santamaria/projects/oasis/sources/v2/oasis-2.owl.
  * [10] M.B. van Riemsdijk, M. Dastani and M. Winikoff, Goals in Agent Systems: A Unifying Framework, in AAMAS 08, International Foundation for Autonomous Agents and Multiagent Systems, 2008, pp. 713–720. ISBN ISBN 9780981738116.
  * [11] D. Cantone, C.F. Longo, M. Nicolosi Asmundo, D.F. Santamaria and C. Santoro, CLARA, 2019\. {https://github.com/dfsantamaria/CLARA}.
  * [12] D. Cantone, C.F. Longo, M. Nicolosi-Asmundo, D.F. Santamaria and C. Santoro, Ontological Smart Contracts in OASIS: Ontology for Agents, Systems, and Integration of Services, in: D. Camacho et al. (eds.), Intelligent Distributed Computing XIV, Studies in Computational Intelligence 1026, Chapter 22, 2022, pp. 237–247.
  * [13] G. Bella, D. Cantone, C.F. Longo, M. Nicolosi-Asmundo and D.F. Santamaria, Blockchains through ontologies: the case study of the Ethereum ERC721 standard in OASIS, in: D. Camacho et al. (eds.), Intelligent Distributed Computing XIV, Studies in Computational Intelligence 1026, Chapter 23, 2022, pp. 249–259.
  * [14] G. Bella, D. Cantone, C. Longo, M. Nicolosi Asmundo and D.F. Santamaria, POC4COMMERCE - Practical ONTOCHAIN for E-Commerce - Project Page, 2021\. {https://github.com/dfsantamaria/POC4COMMERCE}.
  * [15] NGI-ONTOCHAIN, ONTOCHAIN A new software ecosystem for trusted, traceable & transparent ontological knowledge, 2020\. https://ontochain.ngi.eu/.
  * [16] G. Bella, D. Cantone, C. Longo, M. Nicolosi Asmundo and D.F. Santamaria, Semantic Representation as a Key Enabler for Blockchain-Based Commerce, K. Tserpes et al. (Eds.): GECON 2021, Springer Lecture Note in Computer Science 13072 (2021), 1–8.
  * [17] G. Bella, D. Cantone, M. Nicolosi-Asmundo and D.F. Santamaria, A Behaviouristic Semantic Approach to Blockchain-based E-Commerce, 2022, pp. 1–46, unpublished manuscript available from the authors.
  * [18] G. Bella, D. Cantone, M. Nicolosi-Asmundo and D.F. Santamaria, Towards a Semantic Blockchain: a Behaviouristic Approach To Modelling Ethereum, 2022, pp. 1–25, unpublished manuscript available from the authors.
  * [19] J. Hendler, Agents and the Semantic Web, IEEE Intelligent Systems 16(2) (2001), 30–37.
  * [20] M. Hadzic, E. Chang and P. Wongthongtham, Ontology-Based Multi-Agent Systems, Springer Publishing Company, Incorporated, 2014\. ISBN ISBN 3642425496, 9783642425493.
  * [21] D.M. Fritzsche, M. Grüninger, K. Baclawski, M. Bennett, G. Berg-Cross, T. Schneider, R.D. Sriram, M. Underwood and A. Westerinen, Ontology Summit 2016 Communique: Ontologies within semantic interoperability ecosystems, Applied Ontology 12(2) (2017), 91–111.
  * [22] Q. Tran and G. Low, MOBMAS: A methodology for ontology-based multi-agent systems development, in: Inf. Softw. Technol., 50(7-8), 2008, pp. 697–722.
  * [23] M. Cossentino, M. Gleizes, A. Molesini and A. Omicini, Processes Engineering and AOSE, in: Agent-Oriented Software Engineering X, M.-P. Gleizes and J.J. Gomez-Sanz, eds, Springer Berlin Heidelberg, 2011, pp. 191–212.
  * [24] A. Freitas, R.H. Bordini and R. Vieira, Model-driven engineering of multi-agent systems based on ontologies, Applied Ontology 12 (2017), 157–188.
  * [25] F. García-Sánchez, J.T. Fernández-Breis, R. Valencia-García, J.M. Gómez and R. Martínez-Béjar, Combining Semantic Web technologies with Multi-Agent Systems for integrated access to biological resources, Journal of Biomedical Informatics 41(5) (2008), 848–859, Semantic Mashup of Biomedical Data.
  * [26] A. Freitas, A. Panisson, L. Hilgert, F. Meneguzzi, R. Vieira and R. Bordini, Applying ontologies to the development and execution of Multi-Agent Systems, Web Intelligence 15 (2017), 291–302.
  * [27] A. Ciortea, S. Mayer and F. Michahelles, Repurposing Manufacturing Lines on the Fly with Multi-Agent Systems for the Web of Things, in: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC, 2018, pp. 813–822.
  * [28] G. Bajaj, R. Agarwal, P. Singh, N. Georgantas and V. Issarny, A study of existing Ontologies in the IoT-domain, arXiv, 2017\. doi:10.48550/ARXIV.1707.00112. https://arxiv.org/abs/1707.00112.
  * [29] W. Wang, S. De, R. Toenjes, E. Reetz and K. Moessner, A Comprehensive Ontology for Knowledge Representation in the Internet of Things, in: 11th International Conference on Trust, Security and Privacy in Computing and Communications, IEEE, 2012, pp. 1793–1798.
  * [30] S.N. Akshay Uttama Nambi, C. Sarkar, R.V. Prasad and A. Rahim, A Unified Semantic Knowledge Base for IoT, in: World Forum on Internet of Things (WF-IoT), IEEE, 2014, pp. 575–580.
  * [31] World Wide Web Consortium, Web of Things (WoT) Thing Description, 2020\. https://www.w3.org/TR/wot-thing-description/.
  * [32] M. English, S. Auer and J. Domingue, Blockchain Technologies & The Semantic Web: A Framework for Symbiotic Development, in: Lehmann, J., Thakkar, H., Halilaj, L., Asmat, R. (eds.) Computer Science Conference for University of Bonn Students, 2016, pp. 47–61.
  * [33] J. Cano-Benito, A. Cimmino and R. García-Castro, Towards Blockchain and Semantic Web, in: Business Information Systems Workshops, W. Abramowicz and R. Corchuelo, eds, Springer International Publishing, Cham, 2019, pp. 220–231.
  * [34] J. de Kruijff and H. Weigand, Understanding the Blockchain Using Enterprise Ontology, in: Advanced Information Systems Engineering, E. Dubois and K. Pohl, eds, Springer International Publishing, Cham, 2017, pp. 29–43. ISBN ISBN 978-3-319-59536-8.
  * [35] M. Ruta, F. Scioscia, S. Ieva, G. Capurso, A. Pinto and E. Di Sciascio, The Ontology for Agents, Systems and Integration of Services: recent advancements of OASIS, in: Proceedings of the 26th Italian Symposium on Advanced Database Systems (SEBD 2018), S. Bergamaschi, T. Di Noia and A. Maurino, eds, CEUR Workshop Proceedings, Vol. 2161, CEUR-WS.org, 2018, pp. 1–12 (paper 6).
  * [36] H.M. Kim and M. Laskowski, Toward an ontology-driven blockchain design for supply-chain provenance, Int. Syst. in Accounting, Finance and Management 25(1) (2018), 18–27.
  * [37] F. Bergenti, G. Caire, S. Monica and A. Poggi, The First Twenty Years of Agent-Based Software Development with JADE, Autonomous Agents and Multi-Agent Systems 34(2) (2020), article number: 36.
  * [38] A. Ricci, M. Piunti, M. Viroli and A. Omicini, Environment Programming in CArtAgO, in: Multi-Agent Programming: Languages, Tools and Applications, Springer US, Boston, MA, 2009, pp. 259–288.


###### Claim 8.

Let $S=\\{\mathit{succ}_{\Delta}^{k}(\Pi,(0,\dots,0))\mid
k\in\mathbb{N}_{0}\\}$. Let $\mathcal{W}$, $\mathcal{W}^{\prime}$ be fixpoint
variable assignments such that for all fixpoint variables $X$

  * •

$\mathcal{W}^{\prime}(X)$ is invariant under type c) substitutions and

  * •

$\mathcal{W}(X)$ and $\mathcal{W}^{\prime}(X)$ are equivalent on $S$.

Then, $\llbracket\psi\rrbracket^{\Pi}_{\mathcal{W}}$ and
$\llbracket\hat{\psi}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$ are equivalent
on $S$.

As mentioned, Claim 8 is shown by a structural induction:

Case $\psi=[\delta_{j}]_{\pi}$: Let
$v\in\\{\mathit{succ}_{\Delta}^{k}(\Pi,(0,\dots,0))\mid
k\in\mathbb{N}_{0}\\}$. If $v=(0,\dots,0)$, we just need to focus on tests
applied to the initial position. As $\hat{\psi}=\psi$ for these positions,
this case is trivial.

If $v=\mathit{succ}_{\Delta}^{k}(\Pi,(0,\dots,0))$ for some $k>0$, we need to
show that $v_{\pi}\in\llbracket\delta_{j}\rrbracket^{\Pi(\pi)}$ iff
$v_{\pi}\in\llbracket(\lnot\delta\mathcal{U}(\delta\land\delta_{j}))\lor(\delta_{j}\land\lnot\mathcal{F}\delta)\rrbracket^{\Pi(\pi)}$
since the evaluation of the test is independent of all positions other than
$v_{\pi}$. If $v_{\pi}\in\llbracket\delta\rrbracket^{\Pi(\pi)}$, then the test
in $\hat{\psi}$ is equivalent to
$(\lnot\delta\mathcal{U}(\delta\land\delta_{j}))$ which is equivalent to
$\delta_{j}$ and the case is established. If
$v_{\pi}\not\in\llbracket\delta\rrbracket^{\Pi(\pi)}$, then we know that there
are no future positions on $\pi$ that satisfy $\Delta(\pi)$, i.e. $\delta$,
(since $v=\mathit{succ}_{\Delta}^{k}(\Pi,(0,\dots,0))$) and the test in
$\hat{\psi}$ is equivalent to $(\delta_{j}\land\lnot\mathcal{F}\delta)$ which
is equivalent to $\delta_{j}$ and the case is established as well.

Case $\psi=\lnot[\delta_{j}]_{\pi}$: Analogous to the previous case.

Case $\psi=X$: Follows immediately from the assumptions on $\mathcal{W}$ and
$\mathcal{W}^{\prime}$.

Case $\psi=\psi_{1}\lor\psi_{2}$: Follows immediately from the induction
hypothesis.

Case $\psi=\psi_{1}\land\psi_{2}$: Follows immediately from the induction
hypothesis.

Case $\psi=\bigcirc^{\Delta}\psi_{1}$: Let
$v\in\\{\mathit{succ}_{\Delta}^{k}(\Pi,(0,\dots,0))\mid
k\in\mathbb{N}_{0}\\}$. Since $\mathcal{W}^{\prime}(X)$ is invariant under
type c) substitutions for all fixpoint variables $X$, we can apply Claim 7 and
obtain that $\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$
is invariant under type c) substitutions.

On the one hand, assume that
$v\in\llbracket\bigcirc^{\Delta}\psi_{1}\rrbracket^{\Pi}_{\mathcal{W}}$. By
the definition of the semantics, we know that
$\mathit{succ}_{\Delta}(\Pi,v)\in\llbracket\psi_{1}\rrbracket^{\Pi}_{\mathcal{W}}$.
From the induction hypothesis, we know that
$\mathit{succ}_{\Delta}(\Pi,v)\in\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$
as well. For all $\pi$ where $v_{\pi}$ is a position of type a) or b) on
$\Pi(\pi)$, we can apply Claim 5 to obtain
$(\mathit{succ}_{\Delta}(\Pi,v))_{\pi}=(\mathit{succ}_{\Gamma}(\Pi,v))_{\pi}$.
For all $\pi$ where $v_{\pi}$ is a position of type c) on $\Pi(\pi)$,
$(\mathit{succ}_{\Delta}(\Pi,v))_{\pi}$ and
$(\mathit{succ}_{\Gamma}(\Pi,v))_{\pi}$ are non minimal positions of type c)
on $\pi$. Since
$\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$ is invariant
under type c) substitutions, we obtain that
$\mathit{succ}_{\Gamma}(\Pi,v)\in\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$
in both cases. Using the semantics definition, we conclude
$v\in\llbracket\bigcirc^{\Gamma}\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$.

On the other hand, assume that
$v\in\llbracket\bigcirc^{\Gamma}\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$.
By the definition of the semantics, we know that
$\mathit{succ}_{\Gamma}(\Pi,v)\in\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$.
For all $\pi$ where $v_{\pi}$ is a position of type a) or b), we can apply
Claim 5 to obtain
$(\mathit{succ}_{\Gamma}(\Pi,v))_{\pi}=(\mathit{succ}_{\Delta}(\Pi,v))_{\pi}$.
For all $\pi$ where $v_{\pi}$ is a position of type c),
$(\mathit{succ}_{\Gamma}(\Pi,v))_{\pi}$ and
$(\mathit{succ}_{\Delta}(\Pi,v))_{\pi}$ are non minimal positions of type c)
on $\pi$. Since
$\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$ is invariant
under type c) substitutions, we again obtain that
$\mathit{succ}_{\Delta}(\Pi,v)\in\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}$
in both cases. From the induction hypothesis, we thus know
$\mathit{succ}_{\Delta}(\Pi,v)\in\llbracket\psi_{1}\rrbracket^{\Pi}_{\mathcal{W}}$
and therefore
$v\in\llbracket\bigcirc^{\Delta}\psi_{1}\rrbracket^{\Pi}_{\mathcal{W}}$ using
the semantics definition.

Case $\psi=\mu X.\psi_{1}$: For least fixpoints, we use the approximant
characterisation from Section A.2 where $\llbracket\mu
X.\psi_{1}\rrbracket^{\Pi}_{\mathcal{W}}=\bigcup_{\kappa\geq
0}\alpha^{\kappa}(\emptyset)$ for $\alpha$ defined as
$\alpha(V)=\llbracket\psi_{1}\rrbracket^{\Pi}_{\mathcal{W}[X\mapsto V]}$ and
$\llbracket\mu
X.\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}}=\bigcup_{\kappa\geq
0}\hat{\alpha}^{\kappa}(\emptyset)$ for $\hat{\alpha}$ defined as
$\hat{\alpha}(V)=\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W^{\prime}}[X\mapsto
V]}$ We show by transfinite induction, that for all ordinals $\kappa\geq 0$,
(i) $\hat{\alpha}(\emptyset)$ is invariant under type c) substitutions and
(ii) $\alpha^{\kappa}(\emptyset)$ and $\hat{\alpha}^{\kappa}(\emptyset)$ are
equivalent on $S$. In this induction’s base case, $\alpha^{0}(\emptyset)$ and
$\hat{\alpha}^{0}(\emptyset)$ are both empty and thus satisfy both claims.

In the case for successors, the induction hypothesis from the transfinite
induction yields that (1) $\hat{\alpha}^{\kappa}(\emptyset)$ is invariant
under type c) substitutions and (2) $\alpha^{\kappa}(\emptyset)$ and
$\hat{\alpha}^{\kappa}(\emptyset)$ are equivalent on $S$. (1) together with
the fact that $\mathcal{W}^{\prime}(X^{\prime})$ is invariant under type c)
substitutions for all fixpoint variables $X^{\prime}$ means that
$\mathcal{W}^{\prime}[X\mapsto\hat{\alpha}^{\kappa}(\emptyset)](X^{\prime})$
is invariant under type c) substitutions for all fixpoint variables
$X^{\prime}$. Claim 7 then establishes that
$\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}[X\mapsto\hat{\alpha}^{\kappa}(\emptyset)]}=\hat{\alpha}^{\kappa+1}(\emptyset)$
is invariant under type c) substitutions. (2) together with the fact that
$\mathcal{W}(X^{\prime})$ and $\mathcal{W}^{\prime}(X^{\prime})$ are
equivalent on $S$ for all fixpoint variables $X^{\prime}$ yield that
$\mathcal{W}[X\mapsto\alpha^{\kappa}(\emptyset)](X^{\prime})$ and
$\mathcal{W}^{\prime}[X\mapsto\hat{\alpha}^{\kappa}(\emptyset)](X^{\prime})$
are equivalent on $S$ for all fixpoint variables $X^{\prime}$. Since both
requirements on $\mathcal{W}[X\mapsto\alpha^{\kappa}(\emptyset)]$ and
$\mathcal{W}^{\prime}[X\mapsto\hat{\alpha}^{\kappa}(\emptyset)]$ are
fulfilled, the induction hypothesis from the structural induction is
applicable and yields that
$\llbracket\psi_{1}\rrbracket^{\Pi}_{\mathcal{W}[X\mapsto\alpha^{\kappa}(\emptyset)]}=\alpha^{\kappa+1}(\emptyset)$
and
$\llbracket\hat{\psi}_{1}\rrbracket^{\Pi}_{\mathcal{W}^{\prime}[X\mapsto\hat{\alpha}^{\kappa}(\emptyset)]}=\hat{\alpha}^{\kappa+1}(\emptyset)$
are equivalent on $S$.

The case for limit ordinals is a straightforward application of the induction
hypothesis of the transfinite induction.

Case $\psi=\nu X.\psi_{1}$: Analogous to the previous case.

This concludes the proof of Claim 8. $\square$

The inductive step in the main proof is trivial. ∎