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