Keywords :
Argumentation; Automated theorem proving; Dialogue; Higher-order logic; Isabelle/HOL; Knowledge representation and reasoning; Multi-Agent systems; Proof assistants; Semantical embedding; Dialog; Embeddings; High order logic; Isabelle; Isabelle/high-order logic; Multiagent systems (MASs); Proof assistant; Computer Science (all)
Abstract :
[en] 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.
Funding text :
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.
Scopus citations®
without self-citations
1
