Fatio is a dialogue protocol that has been proposed to extend the language for agent communications FIPA ACL with locutions for dialectical argumentation. Its syntax is composed of five agent locutions, and its axiomatic semantics is defined in terms of the mental states (beliefs and desires) of the participating agents, that are influenced by what is uttered. LogiKEy is a framework and methodology for the design and engineering of ethico-legal reasoners which is based on semantical embeddings of logics and logic combinations in expressive classical higher-order logic (HOL). In this paper, we explore a modelling and present a first implementation of the axiomatic semantics of Fatio in the Isabelle/HOL proof assistant system following the LogiKEy methodology.
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 [
LogiKEy [
The rest of the paper is structured as follows: Section 2 describes the Fatio protocol as in [
L1 — Object Logic(s)
This section summarizes the Fatio protocol for dialectical argumentation between agents that has been
introduced in [
The general syntax for utterances is illocution(Pi, ϕ) or illocution(Pi, Pj , ϕ), where illocution
is an illocutionary act, Pi is an identifier for the agent making the utterance (the speaker), Pj (with
Pj 6= Pi) 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 [
The locutions are also subject to combination rules, introduced in [
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 Pi, one dialectical obligations store DOS(Pi) to record dialectical obligations. The contents
of DOS(Pi) are triples (Pi, X, Y ), where Pi is a participant, X ∈ C or X ∈ A, and Y ∈ {+, −}.
The intuition is that (Pi, ϕ, +) ∈ DOS(Pi) indicates that participant Pi has a dialectical obligation to
provide a justification in support of ϕ. Two classes of modal operators are used in the semantics: one
for beliefs Bi and one for desires Di, where i is an agent identifier. Also, an element from FIPA’s action
language is used: Done [illocution(Pi, ϕ), pre-con] indicates that illocution(Pi, ϕ) has been uttered by
participant Pi 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(Pi, ϕ)]. The pre-conditions and
post-conditions are then [
Formally, (Pi, ϕ, +) ∈ DOS(Pi) ∧ (∀k 6= i)(∀j 6= i)(BkDiBj Biϕ). • question(Pj , Pi, ϕ) • challenge(Pj , Pi, ϕ) – Pre-conditions: Some participant Pi(i 6= j) has a dialectical obligation to support ϕ and participant Pj desires that each other participant Pk(k 6= j), believes that Pj desires that Pi utter a justify locution for ϕ. Formally, ∃i(i 6= j) ((Pi, ϕ, +) ∈ DOS(Pi) ∧ (∀k 6= j)Dj BkDj (∃Δ ∈ A) Done [justify(Pi, Δ ⊢+ ϕ)]) . – Post-conditions: Participant Pi must utter a justify locution. There is no change on the dialectical obligations. Formally, (∃Δ ∈ A) Done [justify(Pi, Δ ⊢+ ϕ)] . – Pre-conditions: Some participant Pi(i 6= j) has a dialectical obligation to support ϕ.
Participant Pj desires that each other participant Pk(k 6= j), believe both that Pj desires that Pi utter a justify(Pi, Δ ⊢+ ϕ) locution for some Δ ∈ A and that Pj does not believe ϕ. Formally, ∃i(i 6= j) ((Pi, ϕ, +) ∈ DOS(Pi) ∧ (∀k 6= j)(Dj Bk¬Bj ϕ) ∧ (∀k 6= j)Dj BkDj (∃Δ ∈ A) Done [justify(Pi, Δ ⊢+ ϕ)]). – Post-conditions: Participant Pi must utter a justify locution. Moreover, the dialectical obligation (Pj , ϕ, −) is added to DOS(Pj ). Formally, ((Pj , ϕ, −) ∈ DOS(Pj ) ∧ (∃Δ ∈ A) Done [justify (Pi, Δ ⊢+ ϕ)]). – Pre-conditions: A speaker Pi has a dialectical obligation to support ϕ. Another speaker Pj (j 6= i) has uttered a question(Pj , Pi, ϕ) or a challenge(Pj , Pi, ϕ) locution. Furthermore, Pi desires that each participant Pk(k 6= i) believes that Pi believes that Φ ∈ A is an argument for ϕ. Formally, ((Pi, ϕ, +) ∈ DOS(Pi)) ∧ (Done [question (Pj , Pi, ϕ)] ∨ Done [challenge (Pj , Pi, ϕ)) ∧ (∃Φ ∈ A) (∀k 6= i) DiBkBi (Φ ⊢+ ϕ) . – Post-conditions: Each participant Pk(k 6= i) believes that Pi desires that each participant Pj (j 6= i) believes that Pi believes that Φ ∈ A is an argument for ϕ. Moreover, the dialectical obligation (Pi, Φ, +) is added to DOS(Pi). Formally, ((Pi, Φ, +) ∈ DOS(Pi)) ∧ (∀k 6= i) (∀j 6= i) BkDiBj Bi (Φ ⊢+ ϕ) . – Pre-conditions: For the proposition ϕ ∈ C, it is required that (Pi, ϕ, +) ∈ DOS(Pi).
Participant Pi desires that each participant Pj (j 6= i) believes that Pi no longer believes ϕ. Additionally, Pi desires that each participant Pj (j 6= i) understands that Pi no longer maintains a disbelief in ϕ. Formally, ((Pi, ϕ, +) ∈ DOS(Pi) ∧ (∀j 6= i) DiBj ¬Biϕ) ∨ ((Pi, ϕ, −) ∈ DOS(Pi) ∧ (∀j 6= i) DiBj ¬¬Biϕ) . – Post-conditions: Depending on the case outlined in the pre-conditions, either each participant Pk(k 6= i) believes that participant Pi desires that each participant Pj (j 6= i) believes that Pi no longer believes ϕ, or each participant Pk(k 6= i) believes that participant Pi desires that each participant Pj (j 6= i) believes that Pi no longer disbelieves ϕ. Moreover, either (Pi, ϕ, +) or (Pi, ϕ, −) is removed from DOS(Pi). Formally, ((Pi, ϕ, +) ∈/ DOS(Pi) ∧ (∀k 6= i) (∀j 6= i) BkDiBj ¬Biϕ) ∨ ((Pi, ϕ, −) ∈/ DOS(Pi) ∧ (∀k 6= i) (∀j 6= i) BkDiBj ¬¬Biϕ) .
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.
3. 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 [
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. L3 — Dialogue Applications
L2.2 — Fatio Language
L2.1 — Encoding of
World Knowledge
L1.3 — Logic Combination L1.1 — Content
Logic (Deep Embedding)
L1.2 — BD Logic (Shallow
Embedding)
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.1
We 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 Bi and Di for each speaker i. 1The code of the Isabelle/HOL implementation that we describe here is available at https://github.com/cbenzmueller/LogiKEy/ tree/master/Fatio/v1
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(Pi, ϕ)] (with MapDone) and for Φ ⊢+ ϕ in justify(Pi, Φ ⊢+ ϕ) (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 Dj BkDj in (∀k 6= j)Dj BkDj (∃Δ ∈ A) Done [justify(Pi, Δ ⊢+ ϕ)] . 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 6= j) (∃Δ ∈ A) Dj BkDj Done [justify(Pi, Δ ⊢+ ϕ)] . 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(Pi, Δ ⊢+ ϕ)], 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.
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. This work was supported by the Luxembourg National Research Fund (FNR) through the project Logical methods for Deontic Explanations (INTER/DFG/23/17415164/LODEX) and the project Deontic Logic for Epistemic Rights (OPEN O20/14776480).
The authors would like to thank Prof. Leon van der Torre for sharing the enthusiasm about Fatio, and David Fuenmayor and Daniel Kirchner for helpful comments.