Lamas slides

These (links below) are the slides presented at the LAMAS workshop 2007.


Pietro Abate and Rajeev Goré, Australian National University, A Cut-free Tableau Calculus for the Logic of Common Knowledge

Reasoning about knowledge, in particular about the knowledge of agents who reason about the world and each other's knowledge, plays an important role in several areas of computer science, philosophy, game theory and many other fields. The notion of Common Knowledge (CK), where everybody knows, every- one knows that everyone knows, etc has also proved fundamental in the analysis of interacting groups of agents (see [FHMV95] for an extensive overview).

We focus on the development of a cut-free finitary tableau calculus with histories for n-agent modal logics with common knowledge (LCK). Thus, we get a proof system where proof-search becomes feasible and we lay the basis for developing a uniform framework for the treatment of the family of logics of common knowledge. Our calculus gives a single-pass decision procedure which is space-optimal and uses histories and variables [Gor99, HSZ96, Sch98].

The modularity of the system makes it easy to extend it to the logic of common knowledge based upon T , S4 and S5. An implementation of LCK with two agents using the tableaux workbench (TWB) [AG03] is available at and can be queried over the Internet.


[AG03] P Abate and R Goré. System description: The tableaux workbench (TWB). In TABLEAUX, LNCS, Springer, 2003.

[FHMV95] R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning about Knowledge. The MIT Press, 1995.

[Gor99] R Goré. Chapter 6: Tableau methods for modal and temporal logics. In Handbook of Tableau Methods, pages 297-396. Kluwer, 1999.

[HSZ96] A Heuerding, M Seyfried, and H Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In Proc. TABLEAUX'96, pages 210-225, 1996.

[Sch98] S Schwendimann. A new one-pass tableau calculus for PLTL. In TABLEAUX'98, LNCS 1397:277-291. Springer, 1998.

twb3.pdf513.88 KB
lamas06.pdf87.01 KB