- Technical Program
- Workshops & Tutorials
- At a glance
- Doctoral Consortium
- Opening & Reception
- Best Papers from Sister Conferences Track
- IJCAI Video Track
- Trading Agent Competion (TAC)
- IJCAI-11 Awards
- Funding Opportunities for International Research Collaborations
- General Game Playing Competition
- Banquet
- Ramon Llull Session
- Industry Day
- Closing Event
- List of Accepted Papers
- Poster Boards

Tangled Modal Logic for Spatial Reasoning

David Fernández

We consider an extension of the propositional modal logic S4 which allows $\ps$ to act not only on isolated formulas, but also on sets of formulas. The interpretation of <>G is then given by the tangled closure of the valuations of formulas in G, which over finite transitive, reflexive models indicates the existence of a cluster satisfying G. This extension has been shown to be more expressive than the basic modal language, for example it is equivalent to the bisimulation-invariant fragment of FOL over finite S4 models whereas the basic modal language is weaker. However, previous analyses of this logic have been entirely semantic, and no proof system was previously available.
In this paper we present a sound proof system for the polyadic S4 and prove that it is complete. The axiomatization is fairly standard, adding only the fixpoint axioms of the tangled closure to the usual S4 axioms. The proof proceeds by explicitly constructing a finite model from a consistent set of formulas.