Implementing the Fatio Protocol for Multi-Agent Argumentation in LogiKEy
Abstract
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
Luca Pasetto
PostDoc Researcher
My current research focuses on knowledge representation and automation of reasoning with non-classical and non-monotonic logics, especially with application to the legal context. I am also interested in designing and applying formal techniques to assess and explain the behaviour of non-transparent systems and to check for compliance with regulatory constraints. For more information, please visit my website