Introduction

The rise of artificial assistants has lead to an increased interest in behaviour change support agents [1], which can support the user in establishing new routines and finding ways to achieve their goals consistently. In order for these agents to support each user as effectively as possible, the agents need to model the user's desires, needs and preferences as accurately as possible [2]. Since the agent should offer support over longer periods of time, it is likely that both the user and the surrounding context will go through changes throughout the agent's use [3]. Based on the emerging design principles of hybrid intelligence [4],we propose that the agent and the user should be able to collaborate in order to identify and implement the updates that are necessary to adapt the agent over time. This means that the user is in control of the agent's knowledge and beliefs [5], but the agent should be able to assist the user in determining how each change can be realised and explaining the effects that this will have.

While data-driven approaches such as machine learning, can be used to create a detailed and accurate user model [6], these models can be hard to adapt when the user's needs change [7]. The concepts captured in these user models are often not explicitly represented, which in turn means that they cannot be updated directly. This also makes it difficult for the user to understand exactly how their changes will affect the agent's output [8]. By using knowledge-driven methods, we can formalise changes to the user model within the framework, similarly for example to the work in [7]. In particular, we use default logic to model an agent with both dynamic knowledge and beliefs.

In this paper, we introduce a formal framework for a behaviour support agent which includes a model of the world and the user (Section 3.1). We use this framework to represent the agent's knowledge and beliefs explicitly within a default theory (Section 3.2). We use the defeasible nature of default logic to express beliefs about both the user and the world, which allows the agent to reason with incomplete knowledge and provide advice based on this. In order to make changes to the agent's knowledge and beliefs possible, we define updates to our formal framework (Section 4). These updates are based on existing work on belief revision updates for default logic [9]. We then compare this to previous work on user-agent misalignment [10,11] and showcase how the formal updates can be used to resolve potential misalignment scenarios (Section 5) . Throughout the paper we will illustrate the framework using a simple running example of a support agent intended to assist the user in finding a suitable exercise based on their needs. framework in Section 3.2. We also present the belief revision operators that we will be using in Section 4.

Ordered Default Logic

Default logic was first introduced in [12] to formalise inference rules which are usually true but allow for exceptions. This is done using default rules of the form Prerequisite ∶ Justification Consequent 𝛿 .

This rule states that if the prerequisite is proven and it is consistent to assume the justification, then the consequent is inferred.

In the work of [13] there is additionally a strict partial ordering 𝛿 1 < 𝛿 2 on these default rules which expresses that 𝛿 1 should only be applied if 𝛿 2 has already been applied or is inapplicable. This results in an ordered default theory of the form (𝐾 , 𝐷, <) in which 𝐾 is a set of sentences, 𝐷 is a set of default rules and < is an ordering on the default rules in 𝐷. Intuitively, we understand the sentences in 𝐾 to describe our, possibly incomplete, knowledge of the world while the default rules in 𝐷 allow us to derive additional information based on our beliefs. The ordering < may be used to express either preferences or priorities between these beliefs. A theory of this ordered default logic can be translated into standard default logic, allowing for an implementation in theorem provers for standard default logic [13].

When working with default theories, we are interested in the complete views of the world that are consistent with the initial theory, which we refer to as extensions. For an ordered default theory 𝑇 = (𝐾 , 𝐷, <) and any set of sentences 𝑆, we define Γ(𝑆) to be the smallest set satisfying the following properties:

1. 𝐾 ⊆ Γ(𝑆) 2. 𝑇 ℎ(Γ(𝑆)) = Γ(𝑆) 3. for all default rules 𝛼 ∶ 𝛽 𝛾 ∈ 𝐷, if 𝛼 ∈ Γ(𝑆) and ¬𝛽 ∉ 𝑆 then 𝛾 ∈ Γ(𝑆)

Here 𝑇 ℎ(Γ(𝑆)) stands for the deductive closure of Γ(𝑆). We call a set of sentences 𝐸 an extension of the theory 𝑇 if 𝐸 = Γ(𝐸). In the following, we will discuss only the consistent extensions of a theory. If we restrict ourselves to normal default rules where the justification and the consequent are the same, [12] has shown that this ensures the existence of a consistent extension. In the following, we will only consider default rules of this form. Definition 1. We define ℰ (𝑇 ) to be the set of all consistent extensions of the default theory 𝑇 = (𝐾 , 𝐷, <).

The consistent extensions we have defined above do not yet take the ordering < into account. To include this we use the notion of <-preserving extensions from [13].

Definition 2. We define 𝑃𝑟𝑒𝑟𝑒𝑞(Δ),𝐽 𝑢𝑠𝑡𝑖𝑓 (Δ) and 𝐶𝑜𝑛𝑠𝑒𝑞(Δ) to be the set of prerequisites, justifications and consequents of the default rules 𝛿 in Δ. We take 𝐺𝐷(𝐷, 𝐸) to be the set of default rules which generate the extension 𝐸 and a grounded enumeration (𝛿 𝑖 ) 𝑖∈𝐼 of 𝐺𝐷(𝐷, 𝐸) to be an order in which these rules can be applied.

For a theory 𝑇 = (𝐾 , 𝐷, <), an extension 𝐸 ∈ ℰ (𝑇 ) is <-preserving if there is a grounded enumeration (𝛿 𝑖 ) 𝑖∈𝐼 of 𝐺𝐷(𝐷, 𝐸) so that for all 𝑖, 𝑗 ∈ 𝐼 and 𝛿 ∈ 𝐷 ∖ 𝐺𝐷(𝐷, 𝐸) it holds that

1. if 𝛿 𝑖 < 𝛿 𝑗 then 𝑗 < 𝑖 and 2. if 𝛿 𝑖 < 𝛿 then 𝑃𝑟𝑒𝑟𝑒𝑞(𝛿) ∉ 𝐸 or 𝐾 ∪ 𝐶𝑜𝑛𝑠𝑒𝑞({𝛿 0 , … , 𝛿 𝑖−1 }) ⊢ ¬𝐽 𝑢𝑠𝑡𝑖𝑓 (𝛿).

Even if we know that ℰ (𝑇 ) is not empty, this does not ensure that a <-preserving extension of 𝑇 = (𝐾 , 𝐷, <) exists. Intuitively, this is because lower ranked default rules may have a consequent which can be used to infer the prerequisite of otherwise inapplicable, higher ranked default rules. This means that a higher ranked rule may be applied after the application of a lower ranked rule. As a result, the grounded enumeration of 𝐺𝐷(𝐷, 𝐸) will not satisfy the first condition from Definition 2.

In [14] these inference relationships between the default rules of a theory are formalised using the dependency graph of the theory. The dependency graph 𝒢 (𝐷, 𝐾 ) captures whether default rules influence the applicability of other default rules, either positively by inferring the prerequisite or negatively by inferring the negation of the justification. We take 𝒢 (𝐷, 𝐾 ) to be the set of directed edges between the default rules in 𝐷.

In [13] this is used to specify conditions under which an order default theory has a <-preserving extension. For this, a default theory is considered even if all cycles of the dependency graph have an even number of negative relations. Intuitively this means that the application of a default rules does not negatively influence its own applicability. The ordering < specifies that a lower ranked rule is only applicable after all higher ranked rules have been applied. This means that for each relation (𝛿 < 𝛿 ′ ), we want to ensure that 𝛿 does not affect the applicability of 𝛿 ′ . Proposition 1. As proven in [13], an ordered default theory 𝑇 = (𝐾 , 𝐷, <) is guaranteed to have a <-preserving extension if the dependency graph 𝒢 (𝐷, 𝐾 ) 1. is even and 2. including the ordering < does not create new cycles, so for all cycles

𝒞 of 𝒢 (𝐷, 𝐾 ) ∪ {(𝛿 ′ , 𝛿) | 𝛿 < 𝛿 ′ }, 𝒞 is a cycle of 𝒢 (𝐷, 𝐾 ).

Since the ordering < is not necessarily total, it is possible that there are multiple <-preserving extensions.

Belief Revision

The field of belief revision is concerned with formalising changes to knowledge and belief bases. Since the knowledge and beliefs of a behaviour support agent are subject to change over time, we want to use update operations from belief revision to reflect this.

In general, belief revision is used to update a set of sentences 𝑆. We will be working with theory base revision operators [15], which do not require 𝑆 to be deductively closed, as opposed to AGM operators [16]. Specifically we will use the operator 𝑆 * 𝜑 to add a sentence 𝜑 to 𝑆 while ensuring the resulting set remains consistent and the operator 𝑆 ÷ 𝜑 to remove sentences from 𝑆 until 𝜑 can no longer be inferred.

There is a range of work specifically concerned with integrating belief revision methods into default logic such as [17,18,19]. In our work we will use the operators defined in [9], which includes updates to the knowledge base and the default rules of a default theory.

If we use theory base revision operators, 𝐾 * 𝜑 and 𝐾 ÷𝜑 on the knowledge base 𝐾 of a default theory 𝑇, [9] shows that this can be used to either add 𝜑 to all extensions of 𝑇 or remove 𝜑 from 𝑇 ℎ(𝐾 ).

Additionally, [9] introduces updates on the set of default rules 𝐷. We use 𝐷 ÷𝛿 = 𝐷 ∖{𝛿} as an operator which removes the default rule 𝛿 from 𝐷 and 𝐷 * 𝛿 = 𝐷 ∪ {𝛿} which adds a default rule 𝛿 to 𝐷.

Behaviour Support Agent

In the following section we introduce our framework that can be used to formalise a behaviour support agent. The agent will be able to select a suitable goal for the user to pursue based on the context that the user is currently in. The agent will then recommend actions which result in this goal being achieved, based on the user's preferences.

Syntax

We define a support agent for a set of possible actions 𝐴 that the agent can recommend, the set of goals 𝐺 the user may have and a set of contexts 𝐶 that may affect the user's goals and actions. Definition 3 (Atoms). We define the following sets of propositional atoms:

• 𝐴 = {𝑎 1 , … , 𝑎 𝑛 } describing the possible actions, • 𝐺 = {𝑔 1 , … , 𝑔 𝑚 } describing the goals, • 𝐶 = {𝑐 1 , … , 𝑐 𝑙 } describing different contexts and • 𝐴𝑡𝑜𝑚𝑠 = 𝐴 ∪ 𝐺 ∪ 𝐶.

Definition 4 (Language). Let 𝑂 = {⊤, ¬, ∧, ∨, →} be a standard set of logical operators. We introduce the following propositional languages, defined over the operators 𝑂 and sets of atoms in the usual way:

• The action language ℒ 𝐴 over 𝑂 and atoms 𝐴 • The goal language ℒ 𝐺 over 𝑂 and atoms 𝐺 • The context language ℒ 𝐶 over 𝑂 and atoms 𝐶 • The agent language ℒ over 𝑂 and atoms 𝐴𝑡𝑜𝑚𝑠 A plan for a goal 𝑔 ∈ 𝐺 is a tuple of the form (𝑔, 𝜑), in which 𝜑 is a formula from ℒ 𝐴 describing the actions that must be taken or avoided to achieve the goal 𝑔. Definition 5. The set of all possible plans 𝐿𝑃 is defined as follows: 𝐿𝑃 = {(𝑔, 𝜑) | 𝑔 ∈ 𝐺, 𝜑 ∈ ℒ 𝐴 , 𝜑 ≢ ⊥}.

We introduce several types of rules which allow the agent to infer information based on its initial knowledge. Each rule is represented as a tuple (𝜑, 𝜓 ) in which 𝜑 is the prerequisite and 𝜓 is the consequent. These rules will capture a form of defeasible reasoning in which we only infer the consequent if it is consistent with all other information. This means that if 𝜑 is true and nothing suggests otherwise, then 𝜓 is inferred. For all types of rules 𝜑 may be ⊤ to signify that the rule has no prerequisite.

Context assumption rules are of the form (𝜑, 𝜓 ) with 𝜑, 𝜓 ∈ ℒ 𝐶 describing aspects of the context. We can use these rules to make assumptions about the standard context that the user is in or to represent the beliefs the agent has about the relation between different contexts.

Definition 6. The set of all possible context assumption rules is defined asℛ 𝐶 = {(𝜑, 𝜓 ) | 𝜑, 𝜓 ∈ ℒ 𝐶 }.

Goal selection rules are of the form (𝜑, 𝑔) with 𝜑 ∈ ℒ 𝐶 describing the context and 𝑔 ∈ 𝐺 describing the goal that should be achieved in this context. These are used to describe which goal the user should strive for in a certain context, if possible.

Definition 7. The set of all possible goal selection rules is defined asℛ 𝐺 = {(𝜑, 𝑔) | 𝜑 ∈ ℒ 𝑐 , 𝑔 ∈ 𝐺}.

Action selection rules are of the form (𝜑, 𝜓 ) with 𝜑 ∈ ℒ and 𝜓 ∈ ℒ 𝐴 . Here 𝜑 describes the circumstances in which the actions described in 𝜓 may be taken, if they are possible. These circumstances can include certain context factors, the selected goals and other selected actions depending on the application.

Definition 8. The set of action selection rules is defined asℛ 𝐴 = {(𝜙, 𝜓 ) | 𝜙 ∈ ℒ , 𝜓 ∈ ℒ 𝐴 }.

We use ℛ = ℛ 𝐶 ∪ ℛ 𝐺 ∪ ℛ 𝐴 to refer to all rules collectively. In order to be able to reason with these rules, we assign each rule 𝑟 ∈ ℛ a unique name 𝑛(𝑟). For this, we define an injective naming function 𝑛 from the set of all rules ℛ to a set of names 𝑁. We use these names to define an ordering on the rules. For simplicity of notation we will use the name and the rule itself interchangeably.

We represent the current state of the agent through its configuration, a tuple which specifies the formulas, rules and orderings that the agent reasons with. Definition 9. The configuration of an agent is a tuple Conf = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) where 𝑊 ⊆ ℒ is the world knowledge, 𝐶𝐶 ⊆ 𝐿 𝐶 are literals describing the current context, 𝑃 ⊆ 𝐿𝑃 is a set of plans, 𝐷 𝐶 ⊆ ℛ 𝐶 is a set of context assumption rules, 𝐷 𝐺 ⊆ ℛ 𝐺 is a set of goal selection rules, 𝐷 𝐴 ⊆ ℛ 𝐴 is a set of action selection rules and < 𝐶 , < 𝐺 , < 𝐴 are acyclic orderings on 𝐷 𝐶 , 𝐷 𝐺 and 𝐷 𝐴 .

We also specify that for each goal 𝑔 ∈ 𝐺, there is only one plan 𝑝 = (𝑔, 𝜑) ∈ 𝑃. If there are multiple ways to achieve a goal this should be specified through disjunctions in 𝜑, rather than separate plans.

To illustrate the use of each component of the agent's configuration we introduce a simplified example. We consider an agent which can give the user advice on how to lead a healthier lifestyle based on the user's medical data. For our purposes we assume that the agent should recommend one exercise for the user each day, but if the user's blood pressure is elevated, this should be a higher-intensity workout. The agent knows of two types of low-intensity exercises, namely walking and yoga, and two types of higher-intensity exercises, namely going for a run and weight training.

Example 1. The agent is defined for the context factor 𝐶 = {𝐵𝑃} which indicates that the user's blood pressure is elevated, the set of goals 𝐺 = {𝐿𝐼 , 𝐻 𝐼 } which stand for lowintensity or higher-intensity workouts and the set of actions 𝐴 = {Walk, Yoga, Run, Weights} which are available.

The world knowledge is given by 𝑊 = {𝜑 1𝑔 , 𝜑 1𝑎 }, in which the formulas 𝜑 1𝑔 , 𝜑 1𝑎 express that at most one goal and one action proposition can be true at the same time and therefore included in the agent's advice. This is needed to ensure that the agent only gives one recommended action each day. The current context 𝐶𝐶 contains the blood pressure information of the user. In this example we will assume that the blood pressure is high, so 𝐶𝐶 = {𝐵𝑃}. The plans corresponding to the goals are 𝑃 = {(𝐿𝐼 , 𝑊 𝑎𝑙𝑘 ∨ 𝑌 𝑜𝑔𝑎), (𝐻 𝐼 , 𝑅𝑢𝑛 ∨ 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠)}.

We assume that if we have no information suggesting otherwise, the user's blood pressure is normal. Therefore 𝐷 𝐶 = {(⊤, ¬𝐵𝑃)}. The goal of a higher intensity workout should only be selected if 𝐵𝑃 is true, but the goal of a lower intensity workout can be selected in any situation so 𝐷 𝐺 = {(𝐵𝑃, 𝐻 𝐼 ), (⊤, 𝐿𝐼 )}. For the sake of this example we assume that all the considered actions can be done in any context, which gives us the action selection rules {(⊤, 𝑊 𝑎𝑙𝑘), (⊤, 𝑌 𝑜𝑔𝑎), (⊤, 𝑅𝑢𝑛), (⊤, 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠)}.

Since we only have one context assumption rule, we do not specify any ordering on this type of rule. The goal of a higher intensity workout, if applicable, is more important than the lower intensity workout so we have (⊤, 𝐿𝐼 ) < 𝐺 (𝐵𝑃, 𝐻 𝐼 ) The user has expressed that they prefer Yoga over Walking and Running over Weights so we specify (⊤, 𝑊 𝑎𝑙𝑘) < 𝐴 (⊤, 𝑌 𝑜𝑔𝑎) and (⊤, 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠) < 𝐴 (⊤, 𝑅𝑢𝑛).

This results in an agent configuration 𝐸𝑥 = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 )

Determining the Agent's Advice

For a given configuration Conf of the agent, we define a corresponding theory of ordered default logic 𝑇 = (𝐾 , 𝐷, <). We define the knowledge base 𝐾 based on 𝑊, 𝐶𝐶 and 𝑃, the set of default rules based on 𝐷 𝐶 , 𝐷 𝐺 and 𝐷 𝐴 and the ordering < based on < 𝐶 , < 𝐺 and < 𝐴 . We take the sentences in 𝐾 to describe the agent's, possibly incomplete, knowledge of the world while the default rules in 𝐷 allow the agent to derive additional information based on its beliefs. The ordering < provides a way to prioritise between these beliefs, either based on other beliefs about the world or based on the the user's preferences.

For this we translate every plan 𝑝 ∈ 𝑃 of the form 𝑝 = (𝑔, 𝜑) into a formula 𝑔 → 𝜑 ∈ ℒ. We write 𝑇 𝑟(𝑃) = {𝑔 → 𝜑 | (𝑔, 𝜑) ∈ 𝑃} for the set of all such translated plans. We also translate each rule 𝑟 = (𝜑, 𝜓 ) ∈ 𝐷 𝑖 for 𝑖 ∈ {𝐶, 𝐺, 𝐴} in the agent's configuration to a default rule of the form

𝜑 ∶ 𝜓 𝜓 𝑟 .

We take the transitive closures < + 𝐴 , < + 𝐺 , < + 𝐶 of the orderings to obtain strict partial orderings and define < as the series composition partial order of 𝐷 𝐶 , 𝐷 𝐺 and 𝐷 𝐴 . This means in addition to ordering given in Conf, we also consider all rules regarding the context to be ranked higher than goal and action selection rules and we rank all goal selection rules higher than the action selection rules. We do this to make sure that the agent first considers the context it is in, then selects a goal for the user to pursue and then selects actions based on this. Definition 10. We define the ordered default theory 𝐷𝐿(Conf) corresponding to the agent whose configuration is given by Conf = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) to be 𝐷𝐿(Conf) = (𝐾 , 𝐷, <) where 𝐾 = 𝑊 ∪ 𝐶𝐶 ∪ 𝑇 𝑟(𝑃) is the knowledge base, 𝐷 = {𝜑 ∶ 𝜓 /𝜓 | (𝜑, 𝜓 ) ∈ 𝐷 𝐶 ∪ 𝐷 𝐺 ∪ 𝐷 𝐴 } is the set of default rules that make up the belief base and < is the series partial order of 𝐷 𝐶 , 𝐷 𝐺 and 𝐷 𝐴 .

Based on our definition of a configuration, it is not yet guaranteed that this ordered default theory has a consistent extension. We define valid configurations to be those which do.

Definition 11. A configuration Conf is valid if 𝑊 ∪ 𝐶𝐶 ∪ 𝑇 𝑟(𝑃) is consistent.

Proposition 2. For an ordered default theory 𝐷𝐿(Conf) = (𝐾 , 𝐷, <) based on a valid configuration Conf of an agent, the unordered default theory (𝐾 , 𝐷) has at least one consistent extension.

This follows directly from [12] as, by definition, 𝐾 is consistent and all default rules in 𝐷 are normal. However, as discussed in Section 2, this does not yet guarantee the existence of a <-preserving extension. For this we define the notion of an effective configuration. Definition 12. An agent configuration is effective if it is valid and the ordered default theory 𝐷𝐿(Conf) fulfils the requirements from Proposition 1.

We argue that an agent which is defined in an intuitively sensible way, will fulfil these conditions. If the dependency graph of the theory 𝐷𝐿(Conf) is not even, or goes against the ordering <, then this signifies an implicit inconsistency in the reasoning formalised in the agent. However, these conditions are difficult to formalise for the configuration of the agent, as they require us to consider the default theory. In future work we hope to determine clear requirements for agent configurations which guarantee for the existence of a <-preserving extension.

We use the <-preserving extensions of the default theory 𝐷𝐿(Conf) based on the agent's configuration to determine the advice that the agent should give the user. If there are multiple suitable extensions of 𝐷𝐿(Conf) then the agent requires a way to choose one of these extensions. This requires a meta-logic above the default logic that we have specified, so we will simply assume that such a selection can be made. Definition 13. For an agent with the effective configuration Conf = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) which is translated into the ordered default theory 𝐷𝐿(Conf) with the <-preserving extension 𝐸, the agent's advice consists of the set of selected goals 𝒜 𝐺 = 𝐺 ∩ 𝐸 and the set of recommended actions 𝒜 𝐴 = 𝐿(𝐴) ∩ 𝐸.

We showcase how the advice is obtained from the configuration of an agent by going through the configuration from Example 1.

Example 2. The configuration 𝐸𝑥 as defined in Example 1 is translated into the ordered default theory 𝑇 = (𝐾 , 𝐷, <) with

• 𝐾 = {𝜑 1𝑔 , 𝜑 1𝑎 , 𝐵𝑃, 𝐻 𝐼 → (𝑅𝑢𝑛 ∨ 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠), 𝐿𝐼 → (𝑊 𝑎𝑙𝑘 ∨ 𝑌 𝑜𝑔𝑎)}, • 𝐷 = { ⊤∶¬𝐵𝑃 ¬𝐵𝑃 𝛿 1 , 𝐵𝑃∶𝐻 𝐼 𝐻 𝐼 𝛿 2 , ⊤∶𝐿𝐼 𝐿𝐼 𝛿 3 , ⊤∶𝑊 𝑎𝑙𝑘 𝑊 𝑎𝑙𝑘 𝛿 4 , ⊤∶𝑌 𝑜𝑔𝑎 𝑌 𝑜𝑔𝑎 𝛿 5 , ⊤∶𝑅𝑢𝑛 𝑅𝑢𝑛 𝛿 6 , ⊤∶𝑊 𝑒𝑖𝑔ℎ𝑡𝑠 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠 𝛿 7 } and • < = 𝐷 𝐶 ; 𝐷 𝐺 ; 𝐷 𝐴 = {(𝛿 𝑖 , 𝛿 1 ) | 𝑖 = 2, … , 7} ∪ {(𝛿 𝑖 , 𝛿 𝑗 ) | 𝑖 = 4 … , 7; 𝑗 = 2, 3} ∪ {(𝛿 3 , 𝛿 2 )} ∪ {(𝛿 4 , 𝛿 5 ), (𝛿 7 , 𝛿 6 )}

The default theory (𝐾 , 𝐷) has four possible extensions. We write only the relevant parts of each extension. These are 𝐸 1 = {𝐻 𝐼 , 𝑅𝑢𝑛}, 𝐸 2 = {𝐻 𝐼 , 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠}, 𝐸 3 = {𝐿𝐼 , 𝑌 𝑜𝑔𝑎} and 𝐸 4 = {𝐿𝐼 , 𝑊 𝑎𝑙𝑘}. However, only 𝐸 1 is <-preserving. Therefore the agent's advice consists of the selected goal 𝐻 𝐼 and the recommended action 𝑅𝑢𝑛.

Agent Updates

In the previous section we have defined the configuration of a behaviour support agent and detailed how this determines the advice that the agent gives. In practice, the knowledge and beliefs of the agent change over time, so we need to be able to adapt the configuration of the agent. In this section, we define update operations on the agent's configuration which will allow us to add or remove information from each component individually.

For each of these components, we want the updates to be defined in such a way that the knowledge base 𝑊 ∪ 𝐶𝐶 ∪ 𝑇 𝑟(𝑃) remains consistent. This is necessary to ensure that we obtain a valid configuration as the result of the update. Unfortunately, we cannot always guarantee that the new configuration will also be effective due to the requirements from Definition 12. We will formally define the updates and also highlight such possible problems.

Updates to Knowledge Base

The knowledge base of the agent is made up of the world knowledge 𝑊, the current context information 𝐶𝐶 and the set of plans 𝑃. We want to be able to update these parts individually, but as explained above we have to consider them all to ensure the updates yield a valid configuration.

We can update the world knowledge 𝑊 of the agent by adding a sentence 𝜑 ∈ ℒ using the following update. This means we use the theory base revision operator on 𝑊 and update it with 𝜑 but also with 𝑇 𝑟(𝑃) and 𝐶𝐶. While we remove 𝑇 𝑟(𝑃) and 𝐶𝐶 again afterwards, this approach guarantees that 𝑊 ′ ∪ 𝐶𝐶 ∪ 𝑇 𝑟(𝑃) will be consistent.

If we want to remove a formula from the world knowledge 𝑊, this is unproblematic for the consistency of the knowledge base.

Definition 15. For a configuration Conf

= (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) and a formula 𝜑 ∈ ℒ, we define the update operation Conf ÷ 𝑊 𝜑 = ((𝑊 ÷ 𝜑), 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) to remove 𝜑 from 𝑊 and its deductive closure 𝑇 ℎ(𝑊 ).

We note that by defining the operator in this way, it is possible that 𝜑 is still contained in an extension 𝐸 of 𝐷𝐿(Conf') due to the information in 𝐶𝐶 ∪ 𝑇 𝑟(𝑃) and the rules in 𝐷 𝐶 , 𝐷 𝐺 and 𝐷 𝐴 .

In order to update the current context 𝐶𝐶 we use the following operators, similarly to the ones for 𝑊.

Definition 16. For a configuration Conf

= (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) and context information 𝜑 ∈ 𝐿(𝐶) so that {𝜑} ∪ 𝑊 ∪ 𝑇 𝑟(𝑃) consistent, we define the update operation Conf * 𝐶𝐶 𝜑 = (𝑊 , 𝐶𝐶 ′ , 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) with 𝐶𝐶 ′ = (𝐶𝐶 * (𝜑 ∪ 𝐶𝐶 ∪ 𝑇 𝑟(𝑃))) ∖ (𝑊 ∪ 𝑇 𝑟(𝑃)) Definition 17. For a configuration Conf = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) and context information 𝜑 ∈ 𝐶 ∪ ¬𝐶, we define the update operations Conf ÷ 𝐶𝐶 𝜑 = (𝑊 , (𝐶𝐶 ÷ 𝜑), 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) to remove 𝜑 from 𝐶𝐶.

In order to update the plans 𝑃 by adding or removing a plan 𝜋 = (𝑔, 𝜑) we use similar updates as for the knowledge base. When adding a new plan to 𝑃 we need to ensure that the resulting set of plans only contains at most one plan per goal. This means we have to remove any previous plan (𝑔, 𝜓 ) for the goal 𝑔 before adding (𝑔, 𝜑) to 𝑃. We also make sure that the new information is consistent with the other components of the knowledge base.

Definition 18. For a configuration Conf

= (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) and a plan 𝜋 = (𝑔, 𝜑) ∈ 𝐿𝑃 so that {𝑇 𝑟(𝜋)} ∪ 𝑊 ∪ 𝐶𝐶 consistent, we define the update operation Conf * 𝑃 𝜋 = (𝑊 , 𝐶𝐶, 𝑃 ′ , 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) with 𝑃 ′ = (𝑃 ∖ {(𝑔, 𝜓 )} ∪ {𝜋}) to add 𝜋 to 𝑃.

If we remove a plan 𝜋 = (𝑔, 𝜑) from 𝑃, this will result in a valid configuration. However, it is possible that the goal 𝑔 is still the result of a goal selection rule and may be contained in an extension of 𝐷𝐿(Conf). This means the agent may advise the user to pursue the goal, despite there not being any action recommendation which corresponds to this. For this reason, this update should usually not be performed in isolation in practice.

Definition 19. For a configuration Conf

= (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) and a plan 𝜋 = (𝑔, 𝜑) ∈ 𝐿𝑃, we define the update operations Conf ÷ 𝑃 𝜋 = (𝑊 , 𝐶𝐶, 𝑃 ′ , 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) with 𝑃 ′ = 𝑃 ∖ 𝜋 to remove 𝜋 from 𝑃. Proof. This follows directly from the definitions of * 𝜑 and ÷𝜑 and Proposition 2.

Unfortunately we cannot make the same claim regarding <-preserving consistent extensions. This is because any update to the knowledge base of a theory will affect the dependency graph 𝒢 (𝐷, 𝐾 ) of the theory 𝐷𝐿(Conf).

Updates to the Beliefs

The beliefs of the agent are made up of the context assumption rules 𝐷 𝐶 , the goal selection rules 𝐷 𝐺 and the action selection rules 𝐷 𝐴 . Since all types of rules and their respective orderings are defined and translated in the same way, we will only go through the updates of the context assumption rules in detail, the rest are analogous.

When adding a new context assumption rule to the agent's belief base, it is likely that this belief should also be integrated into the ordering < 𝐶 . However, this is not mandatory and can be done separately with the update operator on < 𝐶 that we introduce below.

Definition 20. For a configuration Conf = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) and a context assumption rule 𝑟 = (𝜑, 𝜓 ) ∈ ℛ 𝐶 we define the update Conf * 𝐷 𝐶 𝑟 = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 ′ 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) where

𝐷 ′ 𝐶 = 𝐷 𝐶 ∪ {𝑟}.

When an existing context assumption rule 𝑟 needs to be removed from 𝐷 𝐶 , then we have to remove it from the ordering < 𝐶 as well. This follows from the requirement that the ordering < 𝐶 should be defined on the set 𝐷 𝐶 . Proof. This follows directly from the definition and Proposition 2, since all default rules are still normal and the knowledge base is still consistent.

Unfortunately, when adding a new rule we cannot guarantee the existence of a <-preserving extension as this rule could generate new cycles in the dependency graph that might not be even. However, when removing a rule this does result in a configuration Conf ′ for which 𝐷𝐿(Conf) has a <-preserving extension. Proposition 3. For an effective configuration Conf = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) where 𝐷𝐿(Conf) has a <-preserving extension and a rule 𝑟 ∈ ℛ 𝐶 , the ordered default theory 𝐷𝐿(Conf ′ ) with Conf ′ = Conf ÷ 𝐷 𝐶 𝑟, also has a <-preserving extension.

Proof. To see this we check the conditions of Proposition 1. Removing a rule from the configuration and thereby removing a default rule from the default theory, cannot create any new cycles in the dependency graph. Since

Conf is an effective configuration, we know that all existing cycles are even, which means that the dependency graph of 𝐷𝐿(Conf ′ ) is even too. Additionally, any cycles that are removed from the dependency graph by removing 𝑟 are also removed from the ordering <, so the ordering cannot introduce any new cycles.

Updates to the Ordering

The ordering of the agent is made up of the orderings < 𝐶 , < 𝐺 and < 𝐴 on 𝐷 𝐶 , 𝐷 𝐺 and 𝐷 𝐴 respectively. We can update each of these orderings individually and only need to ensure that the resulting ordering is acyclic. Since all three orderings of the agent are defined in the same way, we will only go through the updates to the context ordering in detail; the others are analogous.

We can add a relation to < 𝐶 using the following update. When removing a relation (𝑟 1 , 𝑟 2 ) from < 𝐶 , we ideally want to remove the relation from < + 𝐶 to make sure it does not appear in 𝐷𝐿(Conf). However, this may require removing multiple relations from < 𝐶 in the process. Since we have multiple choices for this, we will not include this in the update. If necessary, the ordering will need to be updated multiple times to fully remove the relation from < + 𝐶 .

Definition 23. For a configuration Conf = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < 𝐶 , < 𝐺 , < 𝐴 ) and a relation (𝑟 1 , 𝑟 2 ) with 𝑟 1 , 𝑟 2 ∈ 𝐷 𝐶 we define the update Conf ÷ < 𝐶 (𝑟 1 , 𝑟 2 ) = (𝑊 , 𝐶𝐶, 𝑃, 𝐷 𝐶 , 𝐷 𝐺 , 𝐷 𝐴 , < ′ 𝐶 , < 𝐺 , < 𝐴 ) where < ′ 𝐶 =< 𝐶 ∖{(𝑟 1 , 𝑟 2 )}.

Lemma 3. The update operators Conf * < 𝐶 (𝑟 1 , 𝑟 2 ) and Conf ÷ < 𝐶 (𝑟 1 , 𝑟 2 ) are well-defined. The resulting ordering < ′ 𝐶 is acyclic. If the default theory 𝐷𝐿(Conf) has a consistent extension, then the updated theory will also have a consistent extension.

Proof. This follows directly from definition as the knowledge base is still consistent and the default rules are still normal.

When adding a new relation to the ordering < 𝐶 , this may create new cycles when combined with the dependency graph of 𝐷𝐿(Conf), which means we cannot guarantee that the resulting configuration will be effective. On the other hand, it is obvious that removing a relation does not have this issue, meaning that a useful configuration will be updated to another useful configuration.

Resolving Misalignments

With the framework we introduced, the agent is able to reason about a user model and a world model in order to provide personalised support to the user. By representing this explicitly, the user can interact with and adapt the agent's reasoning process directly using the updates that we have defined in the previous section. We chose to use default logic for this purpose because this allows the user to interact with and adapt the agent's reasoning process directly using the updates that we have defined in the previous section. A revision of the agent's reasoning process is necessary if the agent's advice does not align with the needs and wants of the user because the agent's advice contains either an action 𝑎 or a goal 𝑔 that the user does not agree with. In the following, we refer to these situations as misalignment scenarios, based on [10,11]. In this section we will discuss the causes of misalignments that are identified in [10] and discuss how these can be resolved using the update operators defined in the previous section.

The three causes for these misalignments that are differentiated in [10] are the reasoning process of the agent being wrong, the agent's user model being wrong or something having changed in such a way that the agent needs to adapt to the new situation. For our purposes, we do not need to differentiate whether the misalignments occur due to a change or because of a mistake in the initialisation of the agent. Formally, these are handled the same way in this framework. We will discuss how each of the scenarios can be addressed by updating the configuration of the agent. We will give examples of potential misalignments with the advice provided by the agent we introduced in Example 1 and showcase how the realignment updates affect that configuration.

For the sake of this section we will assume that the agent and the user are able to identify the exact cause of the misalignment together. While this is not a trivial assumption and still a topic of active research, this is not something that can be achieved purely within the logical framework of an agent, making it out of the scope of this paper. For simplicity, we also assume that there is only one misalignment at a time.

Incorrect Reasoning

The reasoning process of the agent is based on logical inference, which cannot be incorrect by itself. However, if the world model of the agent is incorrect, then the agent may draw the wrong conclusions even if the user model is correct. This may refer to either the knowledge or the beliefs about the world, the latter including the prioritisation of these beliefs.

Incorrect World Knowledge

The first misalignment scenario we consider is the situation in which the agent has incorrect knowledge about the world. This means that there is either a sentence 𝜑 ∉ 𝑊 that the agent does not know or the agent incorrectly accepts 𝜑 ∈ 𝑊 as known.

If the agent is missing the information 𝜑, we can update the configuration Conf of the agent using Conf * 𝑊 𝜑. By definition, this update requires 𝜑 to be consistent with 𝐶𝐶 ∪ 𝑇 𝑟(𝑃). If we assume that 𝜑 is the only cause of misalignment then this requirement also makes sense intuitively. In order for the agent to also be able to give advice, there are the additional requirements of the effective configuration. While we have explained above that these requirements are reasonable, they might be hard for the user to understand, especially if the agent becomes more complex. In future work we hope to look into ways to identify problematic cycles in the agents configuration and assist the user in resolving them.

Example 3. In Example 2, we have identified that the agent's advice would be to pursue higher intensity exercising and specifically to go for a run. However, the user may be unable to go for a run because their regular running route is under construction. While this is related to a certain context in a way, which we discuss later on, we can treat this as direct information about the world. This means we update the agent's configuration with 𝐸𝑥 ′ = 𝐸𝑥 * 𝑊 ¬𝑅𝑢𝑛. As a result, {𝐻 𝐼 , 𝑅𝑢𝑛} is no longer an extension of 𝐸𝑥 ′ , and the agent's advice will instead be based on the extension 𝐸 ′ = {𝐻 𝐼 , 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠}.

Next we consider that the agent has wrongly identified the current context 𝐶𝐶. If the mistake concerns a context factor 𝑐 that is already in 𝐶, this can easily be resolved using the updates Conf * 𝐶𝐶 𝑐 and Conf ÷ 𝐶𝐶 𝑐, similarly to the updates to the knowledge base we described above. However, if the user thinks that a new context factor should be considered which is not yet in the language of the agent, then simply adding it to the current context 𝐶𝐶 is not enough. We likely need to add a context assumption rule which specifies whether this context factor is normally assumed to be true or false. Additionally, we probably want to include this context factor in the relevant goal and action selection rules. Since we do not have an update that can modify individual rules, this needs to be achieved by deleting the original rule, then including the modified rule and lastly reinstating the relevant orderings.

Example 4. We consider that the user does not want to go for a run because it is raining. The original configuration of the agent did not account for the context of rain, so we need to perform a series of updates to include this. We begin by adding 𝑅𝑎𝑖𝑛 to the description of the current context using 𝐸𝑥 1 = 𝐸𝑥 * 𝐶𝐶 𝑅𝑎𝑖𝑛. We add a context assumption rule to specify that unless we have other knowledge, we assume it is not raining. We use the update 𝐸𝑥 2 = 𝐸𝑥 1 * 𝐷 𝐶 ⊤∶¬𝑅𝑎𝑖𝑛 ¬𝑅𝑎𝑖𝑛 𝛿 8 . We remove the action selection rule 𝛿 6 which is concerned with running through 𝐸𝑥 3 = 𝐸𝑥 2 ÷ 𝐷 𝐴 𝛿6. We add the modified action selection rule and obtain 𝐸𝑥 4 = 𝐸𝑥 3 * 𝐷 𝐴

¬𝑅𝑎𝑖𝑛∶𝑅𝑢𝑛 𝑅𝑢𝑛

}. We now restore the ordering by including 𝛿 7 < 𝛿 9 . This gives us the final updated configuration 𝐸𝑥 ′ = 𝐸𝑥 5 * < 𝐴 (𝛿 7 , 𝛿 9 )

The resulting default theory 𝐷𝐿(𝐸𝑥 ′ ) only has one <preserving extension 𝐸 ′ = {𝐻 𝐼 , 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠}.

Incorrect Beliefs about the world

The agent's beliefs about the world, modelled as context assumption rules in 𝐷 𝐶 , may also be incorrect.

If a new belief 𝛿 needs to be adopted, then this can be done using the update Conf * 𝐷 𝐶 𝛿. This will cause the dependency graph of the agent to change, which may mean that the resulting configuration is not effective. This brings similar problems as a change in the world knowledge.

A belief 𝛿 can be removed from the agent's configuration with the update Conf ÷ 𝐷 𝐶 𝛿. While this will produce an effective configuration, this may lead to the agent's advice being less specific towards the user's context.

The beliefs about the world may also need to be prioritised differently, by updating the ordering < 𝐶 . While we have introduced updates Conf * < 𝐶 (𝛿 𝑖 , 𝛿 𝑗 ) and Conf ÷ < 𝐶 (𝛿 𝑖 , 𝛿 𝑗 ) to add or remove a relation to the ordering, in practice we will likely want to make more complex changes. While these can all be broken down into multiple applications of the two updates we have defined, this may be too complicated for the user to oversee themselves. Additionally, we also need to make sure that the relation remains acyclic and does not contradict the implicit ordering of the default theory modelled in the dependency graph.

Example 5. So far the agent's configuration has included the context assumption rule 𝛿 1 that unless other information is available, the user's blood pressure is normal. For this we remove the original rule 𝛿 1 using 𝐸𝑥 1 = 𝐸𝑥 ÷ 𝐷 𝐶 𝛿 1 and then add the new rule through 𝐸𝑥 ′ = 𝐸𝑥 1 * 𝐷 𝐶 ⊤∶𝐵𝑃 𝐵𝑃 . This means that even if the agent does not know the blood pressure levels of the user, so 𝐵𝑃 ∉ 𝐶𝐶, it will still recommend higher intensity exercises.

Incorrect User Model

The user model of our agent contains information about the user's goals, the user's possible actions and the preferences regarding these. While humans may have goals and preferences that are not strictly logical, the formal framework of the agent requires the goals to be consistent with the current context and the knowledge about the world and the dependency graph to fulfil the requirements from Proposition 1. The agent will need to collaborate with the user to ensure that the user model is as accurate as possible while still meeting the formal requirements.

Incorrect Goals

The goals of the user are what motivates the advice that the agent gives, but they are also subject to change as the needs and desires of the user develop. Each goal 𝑔 ∈ 𝐺 has to correspond to a plan 𝜋 ∈ 𝑃, so that the agent knows how each goal can be achieved. Additionally, a goal should occur in the consequent of a goal selection rule, otherwise it cannot be considered in the agent's advice. Any changes to the goals of the user therefore have to be captured in the set of plans and the goal selection rules.

If a new goal 𝑔 is added, this goal needs a corresponding plan 𝜋, which can be added with the update Conf * 𝑃 𝜋. Usually we will also add a goal selection rule (𝜑 ∶ 𝑔/𝑔) 𝛿 𝑔 , for a sentence 𝜑 ∈ ℒ 𝐶 describing the context in which the goal can be selected, by Conf * 𝐷 𝐺 𝛿 𝑔 . The goal selection rule will then likely need to prioritised adequately, by adding relations to the ordering < 𝐺 using Conf * < 𝐺 and Conf÷ < 𝐺 . Each of these updates will affect the dependency graph, which means there is a risk that the resulting agent is not effective.

If the user no longer wants to pursue a goal 𝑔, then the relevant goal selection rules as well as their orderings need to be removed using the appropriate update.

If a plan or a goal selection rule needs to be changed, the original rule has to be deleted and the new version needs to be added in separate updates as for updates to the world model. Example 6. We want the agent to consider the additional goal Rest when giving advice. This goal is achieved if no exercise is done, so the plan is 𝜋 = (Rest, ¬𝑊 𝑎𝑙𝑘 ∧ ¬𝑌 𝑜𝑔𝑎 ∧ ¬𝑅𝑢𝑛 ∧ ¬𝑊 𝑒𝑖𝑔ℎ𝑡𝑠). For now we do not have any context requirements for this goal to be selected but we prioritise it above the other goal selection rules. We begin by including the plan 𝑝 in the set of plans using 𝐸𝑥 1 = 𝐸𝑥 * 𝑃 𝑝. We then include the goal selection rule ⊤ ∶ 𝑅𝑒𝑠𝑡/𝑅𝑒𝑠𝑡 𝛿 𝑔 with the update 𝐸𝑥 2 = 𝐸𝑥 1 * 𝐷 𝐺 𝛿 𝑔 . Lastly, we include the relations (𝛿 2 , 𝛿 𝑔 ) and (𝛿 3 , 𝛿 𝑔 ) in the ordering < 𝐺 through the update 𝐸𝑥 ′ = 𝐸𝑥 2 * < 𝐺 {(𝛿 2 , 𝛿 𝑔 ), (𝛿 3 , 𝛿 𝑔 )}. This results in an effective configuration 𝐸𝑥 ′ with the <-preserving extension 𝐸 ′ = {𝑅𝑒𝑠𝑡, ¬𝑊 𝑎𝑙𝑘, ¬𝑌 𝑜𝑔𝑎, ¬𝑅𝑢𝑛, ¬𝑊 𝑒𝑖𝑔ℎ𝑡𝑠}.

Incorrect Actions

The actions that are recommended by the agent are determined by the plans for the selected goals and the action selection rules. The user may either want to change the context prerequisites for selecting certain actions, add a new action selection rule or remove an existing action selection rule. These can each be achieved using the updates Conf * 𝐷 𝐴 and Conf÷ 𝐷 𝐴 . If the preferences of the user regarding the actions need to be changed, this can be handled analogous to the change of the ordering < 𝐶 , using the updates Conf * < 𝐴 and Conf÷ < 𝐶 .

Example 7. In Example 3, the user was not able to go for a run and we added ¬𝑅𝑢𝑛 to the agent's world knowledge. This time we will remove the action selection rule for 𝑅𝑢𝑛 instead. By performing the update 𝐸𝑥 ′ = 𝐸𝑥 ÷ 𝐷 𝐴 𝛿 6 , the action selection rule and its corresponding ordering in < 𝐴 are removed. This leads to the same < −preserving extension as in Example 3, 𝐸 ′ = {𝐻 𝐼 , 𝑊 𝑒𝑖𝑔ℎ𝑡𝑠}. While these updates formally have the same result, they intuitively mean different things. In Example 3 the user is not able to run due to outside circumstances from the world that may be resolved at some point. We can remove ¬𝑅𝑢𝑛 from the knowledge base 𝑊 and are still able to use the previous user model. The update in this example on the other hand removes running as a possible action from the user model, indicating that the user no longer views this as an option.

Discussion

We have introduced a formal framework which can be used to specify the configuration of a behaviour support agent. The configuration can be translated into a theory of ordered default logic and the <-preserving expansions of this theory determine the advice that the agent presents to the user. We have also defined updates on the configuration of the agent which can add or remove information from each of the components. These updates can be used to resolve misalignments between the user and the agent.

In order to use the updates for realignment, it is necessary for the agent and the user to accurately identify the precise cause of the misalignment. While this problem needs to be addressed through communication between the agent and the user [10], we want to facilitate this process using the formal framework of the agent. In future work we hope to study whether the structure of the framework is understandable to users, how we can formally identify potential causes of misalignment and how we can explain problematic cycles in the dependency graph to assist the user in resolving these.

So far we have only included the basic updates which add or remove information from each component of the agent's configuration. However, in [9] there are also other updates on default theories, such as introducing a possibility by ensuring that there is at least one consistent extension which contains a sentence 𝜑. It may be interesting to see whether these updates can be adapted for ordered default logic and what they would mean for the agent's configuration. The updates we have used so far have also each been permanent changes of the agent's configuration. In practice there may be situations which require different advice in the moment but should not be considered in the future. These might require different types of updates to optimise the computational complexity of the agent.

In order to further demonstrate the potential of our framework, we also hope to implement the example agent we have presented in this paper. Since ordered default logic can be translated into regular default logic using the process described in [13], we can use existing solvers for default logic to implement the reasoning of the agent. By combining this with implementations of belief revision operators, we can study how our framework behaves in a real application. For this, we will likely also need to optimise the agent to reduce the computational complexity. A first step for this is to consider the work of [14] which discusses specific types of default theories for which an extension can be found in polynomial time.