Modeling Epistemic Actions in Dynamic Epistemic Logic using Coq (CROSBI ID 566342)
Prilog sa skupa u časopisu | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Maliković, Marko ; Čubrilo, Mirko
engleski
Modeling Epistemic Actions in Dynamic Epistemic Logic using Coq
In this paper we reason about knowledge in multiagent systems composed of intelligent agents by using Coq - a formal proof management system. We use the dynamic logic of common knowledge which is an extension of common knowledge logic with a dynamic operator that enables us to express the epistemic consequences of epistemic actions of agents in the form of agents’ knowledge about the state of the system, knowledge about other agents’ knowledges, higher-order agents’ knowledge and so on, up to common knowledge. We define epistemic actions as a special type in Coq, which allows us to add a general form of interchange principle that connects knowledge and time in systems with perfect recall. As an example of multiagent systems we consider knowledge games defined by van Ditmarsch. To the best of our knowledge, there are no papers in which such games are considered using a Coq proof assistant. We use an axiomatization of such games as given by van Ditmarsch but extended with some new axioms required in our approach. Due to a deficit in implementations grounded in theory which enable players to compute their knowledge in any state of the game, our approach provides a good basis for it.
Multiagent systems; Dynamic logic of common knowledge; Epistemic actions; Coq
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
3-10.
2010.
nije evidentirano
objavljeno
Podaci o matičnoj publikaciji
Central European conference on information and intelligent systems
Varaždin:
1847-2001
Podaci o skupu
Central european conference on information and intelligent systems
predavanje
23.09.2010-25.09.2010
Varaždin, Hrvatska