id: 06195398
dt: j
an: 06195398
au: Poggiolesi, Francesca
ti: From single agent to multi-agent via hypersequents.
so: Log. Univers. 7, No. 2, 147-166 (2013).
py: 2013
pu: Springer (BirkhĂ¤user), Basel
la: EN
cc:
ut: Aumann structures; cut-elimination; decidability; modal logic; multi-agent
systems
ci:
li: doi:10.1007/s11787-012-0047-8
ab: Summary: In this paper we present a sequent calculus for the multi-agent
system $\bold{S5}_m$. First, we introduce a particularly simple
alternative Kripke semantics for the system $\bold{S5}_m$. Then, we
construct a hypersequent calculus for $\bold{S5}_m$ that reflects at
the syntactic level this alternative interpretation. We prove that this
hypersequent calculus is theoremwise equivalent to the Hilbert-style
system $\bold{S5}_m$, that it is contraction-free and cut-free, and
finally that it is decidable. All results are proved in a purely
syntactic way and the cut-elimination procedure yields an upper bound
of $ip_2 (n, 0)$ where $ip_2$ is an hyperexponential function of base
2.
rv: