Metareasoning for multi-agent epistemic logic
Konstantine Arkoudas and Selmer Bringsjord
Abstract:
We present an encoding of a sequent calculus for a multiagent
epistemic logic in Athena, an interactive theorem proving system
for many-sorted first-order logic. We then use Athena as a metalanguage
in order to reason about the multi-agent logic an as object language.
This facilitates theorem proving in the multi-agent logic in several ways.
First, it lets us marshal the highly efficient theorem provers for classical
first-order logic that are integrated with Athena for the purpose
of doing proofs in the multi-agent logic. Second, unlike model-theoretic
embeddings of modal logics into classical first-order logic, our proofs are
directly convertible into native epistemic logic proofs. Third, because we
are able to quantify over propositions and agents, we get much of the
generality and power of higher-order logic even though we are in a first-order
setting. Finally, we are able to use Athena's versatile tactics for
proof automation in the multi-agent logic. We illustrate by developing a
tactic for solving the generalized version of the wise men problem.
BibTeX Entry
@Inproceedings{ArkoudasAndBringsjord2004CLIMA,
author ={K. Arkoudas and S. Bringsjord},
title ={Metareasoning for multi-agent epistemic logics},
booktitle ={Proceedings of the Fifth International Conference on
Computational Logic In Multi-Agent Systems (CLIMA 2004)},
pages ={50--65},
address = {Lisbon, Portugal},
month ={September},
year ={2004}}
Back to the
publication list of Konstantine Arkoudas