Introduction

Recent advancements in dialogue systems based on language models are pushing the boundaries of what is possible in AI-human interaction. The rapid evolution of these technologies can set up the stage for more intuitive and helpful AI systems in everyday life, but at the same time presents a variety of risks. This motivates research on formal dialogue systems, based on logical languages, for which it is possible to formally (and eventually also mechanically) prove relevant properties. In this paper, we explore an Isabelle/HOL modelling of Fatio, a formal dialogue system based on argumentation between multiple agents by following the LogiKEy [1] framework and methodology. For an overview of argumentation-based dialogue, the interested reader can refer to [2].

LogiKEy [1] is a framework and methodology that can be used for the design, engineering and experimentation of reasoning systems, with a focus on ethico-legal applications [3] and normative reasoning [4]. The formal framework of LogiKEy is based on shallow semantical embeddings (SSE) [5] of combinations of various logics in classical higher-order logic (HOL). This meta-logical approach allows the use of off-the-shelf theorem provers and model finders for HOL, and therefore aids designers of ethical intelligent agents by allowing them to employ existing technologies instead of having to face the cumbersome task of developing completely new tools. Additionally, continuous improvements to the theorem provers enhance the reasoning capabilities within LogiKEy without needing extra adjustments. The methodology is represented in Figure 1: the relevant object logics are encoded in HOL and can in turn be used to express domain theories, with the purpose of successively experimenting with concrete applications and examples.

The rest of the paper is structured as follows: Section 2 describes the Fatio protocol as in [6], Section 3 shows its LogiKEy implementation in the Isabelle/HOL proof assistant system, and Section 4 discusses the relevant results and the remaining challenges.

The Fatio Protocol

This section summarizes the Fatio protocol for dialectical argumentation between agents that has been introduced in [6]. The original paper motivates the protocol as an extension of the language FIPA ACL [7] for agent interactions with the goal of addressing the criticism that it lacks a proper theory of argumentation. The authors therefore provide a set of locutions for the requesting and providing of reasons. The intuition is that agents that are proponents or opponents of a claim aim to establish the truth through various locutions or dialectical moves. The protocol is defined with a syntax, an axiomatic semantics, and an operational semantics.

Syntax

The general syntax for utterances is illocution(P i , ϕ) or illocution(P i , P j , ϕ), where illocution is an illocutionary act, P i is an identifier for the agent making the utterance (the speaker), P j (with P j = P i ) denotes an agent at whom the utterance is directed, and ϕ is the content of the utterance. Utterances are intended to be made to the entire group involved in the dialogue. For the content of the utterance, any agreed formal language can be used, but the authors assume that the content layer is represented in a propositional language, with lower-case Greek letters as propositions. The set of well-formed content formulae, closed under the usual connectives, is denoted as C. Since the protocol is used to exchange justifications for claims, some utterances also contain content comprising arguments (e.g., premises and inference-rules), which are represented by upper-case Greek letters. The set of well-formed argument formulae, closed under the usual connectives, is denoted as A, with C ⊂ A.

If ϕ ∈ C is a proposition in the content language and Φ ∈ A is a justification, Φ ⊢ + ϕ is written to indicate that Φ is an argument in support of ϕ, and Φ ⊢ − ϕ to indicate that Φ is an argument against ϕ. In order to keep track of commitments to provide justifications for utterances, the concept of a dialectical obligation is introduced and is used to refer to previous commitments in the dialogue. The syntax is made up of five locutions or dialectical moves [6]:

• F1assert (P i , ϕ): A speaker P i asserts a statement ϕ. By doing so, P i creates a dialectical obligation to provide justification for ϕ, if subsequently required by another participant. • F2question (P j , P i , ϕ): A speaker P j questions a prior utterance of assert(P i , ϕ) and seeks a justification for ϕ. The speaker P j of the question creates no dialectical obligations. • F3challenge(P j , P i , ϕ): A speaker P j challenges a prior utterance of assert(P i , ϕ) and seeks a justification for ϕ. Unlike a question, P j also creates a dialectical obligation on himself to provide a justification for not asserting ϕ, such as an argument against ϕ, if questioned or challenged. Therefore, challenge(P j , P i , ϕ) is considered stronger than question(P j , P i , ϕ). • F4justify (P i , Φ ⊢ + ϕ): A speaker P i , who had previously uttered assert(P i , ϕ) and was then questioned or challenged, is able to provide a justification Φ for the initial statement ϕ.

• F5retract (P i , ϕ): A speaker P i , who had previously made an assertion assert(P i , ϕ) or justification justify(P i , Φ ⊢ + ϕ), can withdraw this statement with the utterance of retract(P i , ϕ) or retract(P i , Φ ⊢ + ϕ), respectively. This removes the earlier dialectical obligation on P i to justify ϕ or Φ, if questioned or challenged.

The locutions are also subject to combination rules, introduced in [8], that constrain when an utterance can be made within the dialogue, ensuring structured interaction based on assertions, questions, challenges, justifications, and retractions. For instance, they ensure that the utterance assert(P i , ϕ) may be made at any time, and that immediately following an utterance of question(P j , P i , ϕ) or challenge(P j , P i , ϕ), the speaker P i of assert(P i , ϕ) must reply with justify(P i , Φ ⊢ + ϕ), for some Φ ∈ A.

Axiomatic Semantics

The axiomatic semantics gives a set of axioms in terms of pre-conditions and post-conditions for each locution of Fatio, and it involves beliefs and desires of the participating agents. Mental states such as beliefs and desires are used in order to be consistent with the axiomatic semantics of FIPA ACL. The concept of a dialectical obligation is also clarified at this point, as the authors introduce, for each participant P i , one dialectical obligations store DOS(P i ) to record dialectical obligations. The contents of DOS(P i ) are triples (P i , X, Y ), where P i is a participant, X ∈ C or X ∈ A, and Y ∈ {+, −}. The intuition is that (P i , ϕ, +) ∈ DOS(P i ) indicates that participant P i has a dialectical obligation to provide a justification in support of ϕ. Two classes of modal operators are used in the semantics: one for beliefs B i and one for desires D i , where i is an agent identifier. Also, an element from FIPA's action language is used: Done [illocution(P i , ϕ), pre-con] indicates that illocution(P i , ϕ) has been uttered by participant P i with content ϕ, and with pre-conditions pre-con true. For the purposes of the current implementation, we do not consider pre-con and use Done [illocution(P i , ϕ)]. The pre-conditions and post-conditions are then [6]:

• assert(P i , ϕ)

-Pre-conditions: A speaker P i does not have yet the dialectical obligation to provide justification for ϕ, and P i desires that each participant P j (j = i) believes that P i believes the proposition ϕ ∈ C. Formally, ((P i , ϕ, +) / ∈ DOS(P i )) ∧ (∀j = i)(D i B j B i ϕ). -Post-conditions: Each participant P k (k = i), believes that participant P i desires that each participant P j (j = i) believe that P i believes ϕ. Moreover, the dialectical obligation (P i , ϕ, +) is added to DOS(P i ).

Formally,

(P i , ϕ, +) ∈ DOS(P i ) ∧ (∀k = i)(∀j = i)(B k D i B j B i ϕ).

• question(P j , P i , ϕ)

-Pre-conditions: Some participant P i (i = j) has a dialectical obligation to support ϕ and participant P j desires that each other participant P k (k = j), believes that P j desires that P i utter a justify locution for ϕ. Formally, ∃i(i = j)

((P i , ϕ, +) ∈ DOS(P i ) ∧ (∀k = j)D j B k D j (∃∆ ∈ A) Done [justify(P i , ∆ ⊢ + ϕ)]

) . -Post-conditions: Participant P i must utter a justify locution. There is no change on the dialectical obligations. Formally, (∃∆ ∈ A) Done [justify(P i , ∆ ⊢ + ϕ)] .

• challenge(P j , P i , ϕ)

-Pre-conditions: Some participant P i (i = j) has a dialectical obligation to support ϕ. Participant P j desires that each other participant P k (k = j), believe both that P j desires that P i utter a justify(P i , ∆ ⊢ + ϕ) locution for some ∆ ∈ A and that P j does not believe ϕ. Formally, ∃i(i = j)

((P i , ϕ, +) ∈ DOS(P i ) ∧ (∀k = j)(D j B k ¬B j ϕ) ∧ (∀k = j)D j B k D j (∃∆ ∈ A) Done [justify(P i , ∆ ⊢ + ϕ)]

). -Post-conditions: Participant P i must utter a justify locution. Moreover, the dialectical obligation (P j , ϕ, −) is added to DOS(P j ). Formally, ((P j , ϕ, −) ∈ DOS(P j ) ∧ (∃∆ ∈ A) Done [justify (P i , ∆ ⊢ + ϕ)]).

• justify(P i , Φ ⊢ + ϕ)

-Pre-conditions: A speaker P i has a dialectical obligation to support ϕ. Another speaker P j (j = i) has uttered a question(P j , P i , ϕ) or a challenge(P j , P i , ϕ) locution. Furthermore, P i desires that each participant P k (k = i) believes that P i believes that Φ ∈ A is an argument for ϕ. Formally, ((P i , ϕ, +) ∈ DOS(P i )) ∧ (Done [question (P j , P i , ϕ)] ∨ Done [challenge (P j , P i , ϕ))

∧ (∃Φ ∈ A) (∀k = i) D i B k B i (Φ ⊢ + ϕ) .

-Post-conditions: Each participant P k (k = i) believes that P i desires that each participant P j (j = i) believes that P i believes that Φ ∈ A is an argument for ϕ. Moreover, the dialectical obligation (P i , Φ, +) is added to DOS(P i ). Formally, ((

P i , Φ, +) ∈ DOS(P i )) ∧ (∀k = i) (∀j = i) B k D i B j B i (Φ ⊢ + ϕ) .

• retract(P i , ϕ)

-Pre-conditions: For the proposition ϕ ∈ C, it is required that (P i , ϕ, +) ∈ DOS(P i ).

Participant P i desires that each participant P j (j = i) believes that P i no longer believes ϕ.

Additionally, P i desires that each participant P j (j = i) understands that P i no longer maintains a disbelief in ϕ. Formally, ((

P i , ϕ, +) ∈ DOS(P i ) ∧ (∀j = i) D i B j ¬B i ϕ) ∨ ((P i , ϕ, −) ∈ DOS(P i ) ∧ (∀j = i) D i B j ¬¬B i ϕ) .

-Post-conditions: Depending on the case outlined in the pre-conditions, either each participant P k (k = i) believes that participant P i desires that each participant P j (j = i) believes that P i no longer believes ϕ, or each participant P k (k = i) believes that participant P i desires that each participant P j (j = i) believes that P i no longer disbelieves ϕ. Moreover, either (P i , ϕ, +) or (P i , ϕ, −) is removed from DOS(P i ). Formally,

((P i , ϕ, +) / ∈ DOS(P i ) ∧ (∀k = i) (∀j = i) B k D i B j ¬B i ϕ) ∨ ((P i , ϕ, −) / ∈ DOS(P i ) ∧ (∀k = i) (∀j = i) B k D i B j ¬¬B i ϕ) .

Operational Semantics

The operational semantics is given in terms of internal decision mechanisms for agents that in the protocol are not specified and are left to be implemented, for example through reasoning methods based on formal argumentation. For instance, a decision mechanism is used by an agent to decide whether to assert a given statement at a given point of the dialogue, and another decision mechanism is used by an agent with a dialectical obligation to justify a statement or argument to identify the best possible justification at a given point of the dialogue. We do not go into more details of the operational semantics here, as for now we only focused on the encoding of the axiomatic semantics.

Fatio in LogiKEy

The possibility of using the existing LogiKEy infrastructure has allowed for rapid prototyping of the Fatio protocol in the Isabelle/HOL proof assistant system [9]. Figure 2 shows the layers of the LogiKEy methodology applied to Fatio. The layers are as follows:

• L0 is the underlying Meta-Logic (HOL) layer;

• L1 represents the combination of object logics: (L1.1) a deeply embedded logic to be used to express the content of the Fatio locutions and (L1.2) a shallowly embedded logic to represent the axiomatic semantics in terms of beliefs and desires; • L2 is about domain-specific languages: (L2.1) is the encoding of world knowledge using L1.2 and (L2.2) is the actual language of Fatio, based on agents uttering locutions; and • L3 is the layer for dialogue applications, that use in turn the L2 languages. The architecture shows that at layer L1 we have both a shallow and a deep embedding of logics, but additionally the situation is even more complex, as the two logics are also nested within each other. We now go through the main parts of the implementation and describe choices and challenges. 1We begin with layer L1.2, showing the higher-order multimodal logic that we then use to represent beliefs and desires of agents. Here, σ is the type of world depended formulas, and complex formulas are built by following the semantics of the logical connectives. This logic is shallowly embedded, and after defining a datatype for speakers (for simplicity, at this moment we list only three possible speakers a, b and c) we define the two modal operators B i and D i for each speaker i.

At layer L1.1 (on the left below) we have a deeply embedded propositional logic, with formulas of type Formula. This logic is then used inside the Fatio language of type FatioL to represent the content of the Fatio locutions: we show the syntax of the Fatio language at layer L2.2 (on the right below), with the five above mentioned kinds of locutions and content of type Formula.

In the axiomatic semantics, the beliefs and desires of the agents are about formulas that have been uttered during the dialogue using the content language, that is, the deeply embedded one. However, the axiomatic semantics is expressed in the shallowly embedded higher-order multimodal logic. Therefore, at layer L1.3 it is necessary to have a mapping between the deeply embedded content formulas (L1.1) and the shallowly embedded higher-order multimodal logic formulas (L1.2). This is built starting from the atoms of the languages with mkHOMMLatom (on the left below) and arriving to the complex formulas with the function Map1 specified on the relative connectives (on the right below). We also map to the higher-order multimodal logic the special formulas that appear in the axiomatic semantics for Done [illocution(P i , ϕ)] (with MapDone) and for Φ ⊢ + ϕ in justify(P i , Φ ⊢ + ϕ) (with MapEntailment).

We show then some experiments to clarify the differences between the deep and the shallow embedding. First, while for the deeply embedded logic of L1.1 we can find a counterexample to show that it does not hold that p → p = ¬⊥, when this is mapped to the shallowly embedded logic of L1.2 we can prove that it holds that Map1(p → p) = Map1(¬⊥) (on the left below). Indeed, the deep embedding is motivated by the need to differentiate two same Fatio locutions that involve different but semantically equivalent formulas of the content language, while with the shallow embedding we cannot distinguish between formulas like p → p and ¬⊥. We can find a counterexample to show that it does not hold that assert(a, p → p) = assert(a, ¬⊥), but also there is a counterexample to show that it does not hold that Done [assert(a, p → p)] = Done [assert(a, ¬⊥)] (on the right below). This is the intended behaviour for Done, as in this case we might be in a dialogue where agent a has asserted ¬⊥ but not p → p.

We proceed now with the modelling of the axiomatic semantics of the protocol. The first ingredient is the dialectical obligations store DOS, that we represent as a list of triples (Speaker, Formula, Sign). The function to update DOS when a Fatio locution is executed is then shown below here on the right: assert, justify, and challenge add an element to DOS, retract removes an element from DOS, while question does not change DOS.

For layer L1.3, the next step is to encode the pre-conditions of each locution. In order to do that, the formal definitions of the original paper should be clear and not leave space for ambiguity. If we consider the pre-conditions of question and challenge, we have that ∃∆ appears after the modal operators

D j B k D j in (∀k = j)D j B k D j (∃∆ ∈ A) Done [justify(P i , ∆ ⊢ + ϕ)] .

It is not completely clear if the authors actually intended the modal operators to operate on a quantified formula, or if they intended the existential quantifier as a meta-language element. To better understand the situation, we experimented with the expression and tried to move the existential quantifier outside of the modal operators, obtaining (∀k = j) (∃∆ ∈ A) D j B k D j Done [justify(P i , ∆ ⊢ + ϕ)] . Indeed, the two formulas are not equivalent, and we found out that while the second one implies the first one (lemma ent3), the inverse does not hold (counterexample for lemma ent2). For now, we decided to follow strictly the contents of the paper, so we kept the first formula for the pre-conditions, but this might be a knowledge representation choice that can be changed in favor of the formula that better encodes the desired effects.

We can then proceed with the encoding of the pre-conditions. We write function PreCond that checks whether the pre-conditions of a locution are satisfied, given a current dialectical obligations store DOS and a current set Γ of shallowly embedded formulas that represent the encoded world knowledge of layer L2.1.

The post-conditions are encoded with the GammaAdd function, that takes a locution and gives the set of formulas representing its post-conditions. At this point, in the axiomatic semantics of the paper the postconditions of question and challenge contain a formula (∃∆ ∈ A) Done [justify(P i , ∆ ⊢ + ϕ)], which means that the relevant justify locution is uttered. However, we think that this would be better handled by combination rules or operational semantics, and the justify locution cannot have been uttered already when the post-conditions of question and challenge are imposed. For this reason, we simplified the post-conditions of these two locutions.

The actual evolution of the set of formulas Γ is encoded by GammaUpdate, that outputs the updated set of formulas Γ ′ given a current locution and a current set of formulas Γ. It does so by including (1) the new formulas added with GammaAdd, (2) the formulas that are already in Γ and are consistent with (1), and (3) the relevant MapDone formula for the current locution.

A FatioState is defined as a triple (FatioL list, DOS list, Γ). The function FatioCheck goes from one FatioState to the next by executing its first locution, and the function FatioCheckRec executes an entire dialogue by a series of recursive calls, and outputs True if the final state is successful, that is, the pre-conditions of each executed locution are satisfied after having imposed the post-conditions of the previous locution.

Discussion

We presented a first modelling and implementation of the Fatio protocol in the LogiKEy framework. The next step is obviously to carry out more extensive experiments on it, in order to test it and possibly to improve it accordingly. At this point, we ran only a few experiments with some small dialogues. While the reasoning system is promising, and up to our knowledge it is the first implementation of Fatio that actually uses the intended modal logic semantics, the modelling is not simple and there are a few sources of complexity that emerged:

• complexity of the relationship between the embeddings of the logics (the deep embedding is being mapped to the shallow embedding, and the Fatio language, that uses the deeply embedded logic, is again being mapped to the shallow embedding); • complexity in terms of how Isabelle/HOL can cope with the modelling, as we had a few technical issues related to the parsing of the formulas combining different logics, and in order to solve them at this point we are using a large quantity of brackets to speed-up the disambiguation process, and we had some issues regarding the responsiveness of the theorem provers called by sledgehammer, caused by the complexity of the involved formulas; • complexity in terms of human usability/readability for experimentation (the formulas to be used to encode the world knowledge and to satisfy the pre-conditions in the axiomatic semantics involve complex nesting of beliefs and desires that might be hard to grasp for a human user of the protocol, and moreover as already mentioned the formulas have to involve large numbers of brackets to help the parser).

An additional challenge in this kind of work is that in the original paper there are extra-logical aspects that have to be clarified in order to implement the protocol. As it is natural with implementations, there are differences between the paper and the code, and during the implementation things can be simplified or might need to be made more explicit. In our case, for example, we simplified the post-conditions of question and challenge, and we modelled the dialectical obligations store DOS in a slightly simpler way compared to the original paper. At the same time, we had to make (temporary) choices about how to model the Done operator and on where to put the existential quantifier in the pre-conditions of question and challenge. These are cases where the experimental approach proposed with LogiKEy can be impactful, as we made these choice with the support of small experiments.

The point of how to assess the correctness of our method is important to discuss. A pen and paper proof would be possible if we had a proper target semantics, but in the process of implementing the protocol we actually had to make changes to the original semantics. Therefore, a contribution of this paper is in making more clear how the target semantics should look like, so to possibly simplify it. In general, an overall future goal is to simplify the modelling to solve some of the challenges listed above. For instance, as already stated, the relationship between the shallow and the deep embedding is not straightforward. Therefore, streamlining it (e.g., by only using a shallow embedding, even though a more sophisticated one) would help to fix some of the complexities we have with the integration of the different reasoning mechanisms.