\documentclass{entcs}
\usepackage{entcsmacro}
\usepackage{graphicx}
\usepackage{mathpartir}
\usepackage{amsmath,amssymb}
\usepackage{pstricks}
\newcommand{\hearts}{\heartsuit}
\newcommand{\prems}{\mathit{prems}}
\newcommand{\eval}{\mathit{eval}}
\input{header}
\sloppy
% The following is enclosed to allow easy detection of differences in
% ascii coding.
% Upper-case A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
% Lower-case a b c d e f g h i j k l m n o p q r s t u v w x y z
% Digits 0 1 2 3 4 5 6 7 8 9
% Exclamation ! Double quote " Hash (number) #
% Dollar $ Percent % Ampersand &
% Acute accent ' Left paren ( Right paren )
% Asterisk * Plus + Comma ,
% Minus - Point . Solidus /
% Colon : Semicolon ; Less than <
% Equals =3D Greater than > Question mark ?
% At @ Left bracket [ Backslash \
% Right bracket ] Circumflex ^ Underscore _
% Grave accent ` Left brace { Vertical bar |
% Right brace } Tilde ~
% A couple of exemplary definitions:
%\newcommand{\Nat}{{\mathbb N}}
%\newcommand{\Real}{{\mathbb R}}
\newcommand{\COLOSS}{{\textrm CoLoSS}}
\def\lastname{Hausmann and Schr\"oder}
\begin{document}
\begin{frontmatter}
\title{Heterogenous modal logics within \COLOSS}
\author[DFKI]{Daniel Hausmann\thanksref{myemail}}
\author[DFKI,UBremen]{Lutz Schr\"oder\thanksref{coemail}}
\address[DFKI]{DFKI Bremen, SKS}
\address[UBremen]{Department of Mathematics and Computer Science, Universit\"at Bremen, Germany}
% \thanks[ALL]{Work forms part of DFG-project \emph{Generic Algorithms and Complexity
% Bounds in Coalgebraic Modal Logic} (SCHR 1118/5-1)}
\thanks[myemail]{Email: \href{mailto:Daniel.Hausmann@dfki.de} {\texttt{\normalshape Daniel.Hausmann@dfki.de}}}
\thanks[coemail]{Email: \href{mailto:Lutz.Schroeder@dfki.de} {\texttt{\normalshape Lutz.Schroeder@dfki.de}}}
\begin{abstract}
abstract hier, abstract da
\end{abstract}
\begin{keyword}
Coalgebraic modal logic, heterogenous modal logic, automated reasoning
\end{keyword}
\end{frontmatter}
\section{Introduction}\label{intro}
\ldots
\section{Generic Sequent Calculi for Coalgebraic Modal Logic}
\ldots
\section{Generic and Heterogenous Sequent Calculi for Coalgebraic Modal Logic}
There are several reasonable concepts of what a heterogenous modal logic could be. For the remainder
of this paper we go with the following definition:
\begin{definition}
Given a set $\mathcal{P}$ of atoms, the set $Prop(\mathcal{F})$ of \emph{propositional formulas} over
a set $\mathcal{F}$ of other formulas is defined as follows ($p\in\mathcal{P}$, $\xi\in\mathcal{F}$):
\begin{quote}
$\phi,\psi::= p\mid \phi\wedge\psi\mid\neg\phi\mid \xi$
\end{quote}
Furthermore, given a modal similarity type $\Lambda$, the set $Mod^\Lambda(\mathcal{F})$ of \emph{modal formulas}
over a set $\mathcal{F}$ of other formulas is defined as follows (where $\hearts$ is a $n$-ary operator
from $\Lambda$ and $\psi_1,\ldots,\psi_n\in\mathcal{F}$):
\begin{quote}
$\phi::= \hearts(\psi_1,\dots,\psi_n)$
\end{quote}
\end{definition}
Using the previous definition which provides us with the notion of \emph{layers} of a formula,
we may now fix our concept of heterogenous modal logics:
\begin{definition}
A \emph{heterogenous modal logic} consists of formulas that show a precisely defined constellation
of layers. Given a finite list $\mathcal{M}=[\Lambda_1,\ldots,\Lambda_n]$ of modal similarity
types, formulas $Het(\mathcal{M})=\phi^1$ of the according heterogenous modal logic are defined by circular induction:
\begin{quote}
$\phi^{(i \mod n)}::=Prop(Mod^{\Lambda_{(i\mod n)}}(\phi^{((i+1) \mod n)}).$
\end{quote}
\end{definition}
This definition divides a formula into distinguished \emph{modal layers} (which appear in the
order given by $\mathcal{M}$), with a
\emph{propositional layer} between every two modal layers.
\begin{remark}
Observe that this definition of heterogenous modal logics subsumes the case of modal logics
for composed functors (for given functors $F_1$ to $F_n$ (with associated modal logics)
of suiting arities, the composed modal logic is just the logic associated with
$F_1\circ\ldots\circ F_n$).
Use the above definition and set all (except the first) propositional layers to be the
identity.
\end{remark}
\begin{example}[Heterogenous Formulas]
Let $\mathcal{M}=\{\Lambda_1,\Lambda_2\}$ where $\Lambda_1=\{\Box_{KD}\}$ and
$\Lambda_2=\{\Box_{K}\}$. The formulas of the according heterogenous modal logic
then contain alternating appearences of the two modal operators $\Box_{KD}$ and
$\Box_{K}$, such as in the following examplary formulas:
\begin{quote}
$\phi=\Box_{KD}\Box_{K}\Box_{KD}\Box_{K}\top$\\
$\psi=(\Box_{KD} \Box_{K} ((\Box_{KD} \bot) \vee \top)))\wedge(\Box_{KD}\neg \Box_{K} \top)$
\end{quote}
\end{example}
\begin{definition}
A \emph{formula of level $i$} is a formula whose top-level modalities are all from $\Lambda_i$.
A \emph{heterogenous sequent} is a heterogenous list of formulas of possibly varying levels.
A \emph{heterogenous premise} is just a list of lists of heterogenous sequents.
\end{definition}
We now proceed by introducing a generic sequent calculus that allows for the treatment of
heterogenous modal logics allthewhile restricting our attention to the propositional
portion of the rules at first. The calculus makes use of several \emph{inference rules} each of
which consists of a number of heterogenous premises accompanied by one heterogenous sequent
(refered to as the \emph{conclusion} of the rule).
In order to cope with the increased complexity of the process of proving (or refuting)
possibly heterogenous modal formulas, we are free to assign a level $i$ to each formula
$\psi$ (with the obvious meaning that all top-level modalities in $\psi$ are from
$\Lambda_i$, i.e. $\psi=\phi^i$). The fact that level $i$ is assigned to a formula $\psi$
is denoted by $\psi:i$.
So now we are ready to define the propositional inference rules of the generic sequent
calculus. In order to allow for an efficient implementation of the calculus, it is
reasonable to conceptually section these rules into a group of \emph{linear rules}
(as depicted in Fig.~\ref{fig:linear}) and a group of \emph{closing or branching
rules} (as shown in Fig.~\ref{fig:branch}).
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {$\neg\neg$})\inferrule{\Gamma, A_{:i}}
{\Gamma, \neg\neg A_{:i}}
(\textsc {$\neg\wedge$})\inferrule{\Gamma, \neg A_{:i}, \neg B_{:i}}
{\Gamma, (\neg (A\wedge B))_{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The linear sequent rules}
\label{fig:linear}
\end{figure}
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {$\neg$F})\inferrule{ }
{\Gamma, \neg\bot_{:i}}
(\textsc {Ax})\inferrule{ }
{\Gamma, p_{:i}, \neg p_{:i}}
(\textsc {$\neg\wedge$})\inferrule{\Gamma, A_{:i} \\ \Gamma, B_{:i}}
{\Gamma, (A\wedge B)_{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The closing or branching sequent rules}
\label{fig:branch}
\end{figure}
Take note of the fact that the propositional sequent rules do not interfere
with the level of any involved formulas, i.e. the modal level of formulas
in the premises and the modal level of formulas in the conclusion are the
same.
However, the sequent rules for modal operators may change the level of the
involved formulas. One examplary modal rule is shown in Fig.~\ref{fig:modalK}.
This rule has a homogenous (subset of a) sequent of level $i$ as its
conclusion whereas the only premise consists of one homogenous sequent of level
$i+1$. For this reason the rule realizes a \emph{one-level-step}
(from level $i$ to level $i+1$) upon application during proof search.
For now we consider only homogenous modal rules that realize one-level-steps. Take note that
the resulting logic still is heterogenous since different homogenous logics are combined
together.
\begin{remark}
Heterogenous rules are defined to have rules of different levels in their premises and/or
their conclusion. What's a reasonable example of this case? Are these logics covered by
the coalgebraic theory?
\end{remark}
Put P, G etcpp here!
\begin{example}
Here are some modal rules, adopted to the heterogenous setting:
\begin{enumerate}
\item
The rule for monotone modal logic \textbf{Mon}:
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {\textbf{Mon}})\inferrule{ (\neg A,B)^{:i+1}}
{\Gamma, (\neg \Box A, \Box B)^{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The modal rule for \textbf{Mon}}
\label{fig:modalMon}
\end{figure}
\item
The rule for the modal logic \textbf{K} (i.e. Kripke semantics):
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {\textbf{K}})\inferrule{ (\neg A_1,\ldots,\neg A_n, A_0)^{:i+1}}
{\Gamma, (\neg\Box A_1,\ldots,\neg\Box A_n,\Box A_0)^{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The modal rule for \textbf{K}}
\label{fig:modalK}
\end{figure}
\item
The rule for the modal logic \textbf{KD}:
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {\textbf{KD}})\inferrule{ (\neg A_1,\ldots,\neg A_n, A_0)^{:i+1} \\ (\neg A_1,\ldots,\neg B_n)^{:i+1}}
{\Gamma, (\neg\Box A_1,\ldots,\neg\Box A_n,\Box A_0)^{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The modal rule for \textbf{KD}}
\label{fig:modalKD}
\end{figure}
\item
The rule for Hennessy-Milner logic ($\mathcal{HML}$):
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {$\mathcal{HML}$})\inferrule{ (\neg A_1,\ldots,\neg A_n, A_0)^{:i+1}}
{\Gamma, (\neg[a]A_1,\ldots,\neg[a]A_n,[a]A_0)^{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The modal rule for $\mathcal{HML}$}
\label{fig:modalHML}
\end{figure}
\item
The rule for Pauly's coalition logic (\textbf{C}),
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {\textbf{C}})\inferrule{ (\neg A_1,\ldots,\neg A_n, B)^{:i+1} \\ (D_1,\ldots,D_m)^{:i+1}}
{\Gamma, (\neg[C_1]A_1,\ldots,\neg[C_n]A_n,[D]B,[N]D_1,\ldots,[N]D_m)^{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The modal rule for \textbf{C}}
\label{fig:modalC}
\end{figure}
where $m,n\geq 0$ with the side condition that the $C_i$ are pairwise disjoint subsets of $D$.
\item The rules for basic conditional logic (\textbf{CK}) and for conditional logic with
conditional excluded middle (\textbf{CKCEM}):
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {\textbf{CK}})\inferrule{ (A_0=A_1;\ldots;A_n=A_0)^{:i+1}\\(\neg B_1,\ldots,\neg B_n,B_0)^{:i+1}}
{\Gamma, (\neg A_1\Rightarrow B_1,\ldots,\neg A_n\Rightarrow B_n, A_0\Rightarrow B_0)^{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The modal rule for \textbf{CK}}
\label{fig:modalCK}
\end{figure}
\begin{figure}[!h]
\begin{center}
\begin{tabular}{| c |}
\hline
\\[-5pt]
(\textsc {\textbf{CKCEM}})\inferrule{ (A_0=A_1;\ldots;A_n=A_0)^{:i+1}\\(B_0,\ldots,B_j,\neg B_{j+1},\ldots,\neg B_n)^{:i+1}}
{\Gamma, (A_0\Rightarrow B_0,\ldots,A_j\Rightarrow B_j,\neg A_{j+1}\Rightarrow B_{j+1},
\ldots,\neg A_n\Rightarrow B_n)^{:i}} \\[-5pt]\\
\hline
\end{tabular}
\end{center}
\caption{The modal rule for \textbf{CKCEM}}
\label{fig:modalCKCEM}
\end{figure}
\end{enumerate}
\end{example}
heterogenous sequent algorithm
\section{Implementation}
\section{Generic and Heterogenous Optimisation}
\section{Conclusion}
\ldots
\bibliographystyle{myabbrv}
\bibliography{coalgml}
\end{document}