text:
\section{Conclusions and Further Work}\label{sec:conclusion}

The notion of symmetry has been well studied in propositional logic,
and various optimizations of decision procedures based on it are
known.  In this article, we extend the notion of syntactic and
semantic symmetries to many different modal logics using the framework
of coinductive models.  The main contribution is that a
symmetry $\sigma$ preserves entailments whenever the class is closed
by $\sigma$.  For example, arbitrary  symmetries preserve
entailments in the basic modal logic, but for the hybrid logic
$\mathcal{H}(@)$ we can only consider symmetries that map nominals to
nominals.  The second contribution of the paper is to show that if the
class of models is closed under trees, then the more flexible notion
of layered symmetry also preserve entailments.

To arrive at the previous results, we defined the concept of
$\sigma$-simulation and showed that it preserves $\sigma$-permutation
of formulas.  We then presented permutation sequences $\bar{\sigma}$,
and $\bar{\sigma}$-simulations. Permutation sequences are relevant in
those classes of models that are closed under trees.  This property
enables the use of layered symmetries, a notion that can capture more
symmetries than the ordinary symmetry definition. Indeed, layered
symmetries can be detected independently within atoms at each modal
depth of a formula.  $\bar{\sigma}$-simulations extend the notion of
$\sigma$-simulations to permutation sequences, and enabled us to prove
that layered symmetries also preserve entailment.

Finally, we presented a method to detect symmetries in modal formulas
that reduces the problem to the graph automorphism problem. Given a
formula $\varphi$, the idea is to build a graph in such a way that the
automorphism group of the graph is isomorphic to the symmetry group of
the formula that generated it. A general construction algorithm, suitable for
many modal logics, was presented and its correctness proved.
The presented graph construction algorithm can be extended to detect
layered symmetries. Preliminary results on modal symmetries
concerning this last construction can be found in~\cite{orbe2012}
where we developed an efficient algorithm to detect symmetries for the
basic modal logic, and empirically verified that many modal problems (both randomly and hand generated) contain
symmetries.

Our ongoing research focuses on the incorporation of symmetry
information into a modal tableau calculi such
as~\cite{KaSmoJoLLI2009,hoffmann2010tab} or modal resolution calculi
such as~\cite{arec:reso08}.
One promising theme that we will investigate in the future is
permutations involving also modal literals.

\section{Modal Logics and Coinductive Models} \label{sec:defs}

In what follows, we will assume basic knowledge of classical modal
logics and refer the reader to~\cite{MLBOOK,BBW06} for technical
details.  The coinductive framework for modal logics was introduced
in~\cite{arec:coin10} to investigate normal forms for a wide number of
modal logics.  Its main characteristic is that it allows the
representation of different modal logics in a homogeneous form.
For a start, the set of formulas is as for the basic (multi) modal
logic.

\begin{definition}[Modal formula]\label{modalformula}
  A modal signature is a pair $\tup{\textsf{Atom}\xspace, \textit{Mod}}$ where \textsf{Atom}\xspace
  and \textit{Mod} are two countable, disjoint sets. We usually assume that
  $\textsf{Atom}\xspace$ is infinite. The set of modal formulas over $\langle
  \textsf{Atom}\xspace,$ $\textit{Mod} \rangle$ is defined as
$$
\varphi ::= a \mid \lnot \varphi \mid \varphi \lor \varphi \mid
\boxr{m}\varphi,
$$

\noindent
for $a \in \textsf{Atom}\xspace$, $m \in \textit{Mod}$. $\top$ and $\bot$ stand for
an arbitrary tautology and contradiction, respectively. Connectives such
as $\land, \to$ and $\diamr{m}$, are defined as usual.
\end{definition}

We will define a symmetry as a permutation of literals that
preserve the structure of formulas in conjunctive normal form (CNF).

\begin{definition}[Literals and modal CNF]
  A \emph{literal} $l$ is either an atom $a$ or its negation $\neg a$.  The
  set of literals over $\textsf{Atom}\xspace$ is $\textsf{ALit}\xspace = \textsf{Atom}\xspace \cup \{\neg a \mid a
  \in \textsf{Atom}\xspace\}$.

  A modal formula is in \emph{modal conjunctive normal form (modal
    CNF)} if it is a conjunction of modal CNF clauses. A \emph{modal
    CNF clause} is a disjunction of atoms and modal literals. A
  \emph{modal literal} is a formula of the form $\boxr{m} C$ or $\neg
  \boxr{m} C$ where $C$ is a modal CNF clause.  Every modal formula
  can be transformed into an equisatisfiable formula in modal CNF in
  polynomial time (see~\cite{arec:coin10,sebastiani} for details).
\end{definition}

A formula in modal CNF can be represented as a set of modal CNF clauses
(interpreted conjunctively), and each clause can be
represented as a set of atom and modal literals
(interpreted disjunctively).  With the set representation we can
disregard the order and multiplicity in which clauses and literals
appear.  This will be important when we define symmetries below. In the rest
of the paper we will assume that modal formulas are in modal CNF, and
we will refer to them as modal CNF formulas.

\begin{example}
The modal formula $\varphi = \diamr{m}(p \wedge q \wedge p) \wedge
\boxr{m} \neg r$ is equisatisfiable to the modal CNF formula $ \varphi' =\{ \{ \neg \boxr{m}
\{ \neg p, \neg q \} \} , \{ \boxr{m} \{\neg r \}\} \}$.
\end{example}

Up to now, we have not departed from the standard presentation of
classical modal logic in important ways.  The main change introduced
by the coinductive approach is with the definition of model and
semantic conditions.

\begin{definition}[Models]\label{models}
  Let $\mathcal{S}\xspace = \tup{\textsf{Atom}\xspace, \textit{Mod}}$ be a modal signature and $W$ be a
  fixed, non-empty set. $\mathbf{Mods}_{W}$, the class of all models with
  domain $W$, for the signature $\mathcal{S}\xspace$, is the class  of all tuples
  $\tup{w, W, V, R}$ such that $w \in W$, $V(v) \subseteq \textsf{Atom}\xspace$ for
  all $v \in W$, and
$$
R(m,v) \subseteq \mathbf{Mods}_{W} \mbox{\ for $m \in \textit{Mod}$ and $v \in W$.}
$$

\noindent
Given a model $\mathcal{M}\xspace = \tup{w, W, V, R}$ we will say that $w$ is the
point of evaluation and denote it as $w^\mathcal{M}\xspace$, $W$ is the domain and
denote it as $|\mathcal{M}\xspace|$, $V$ is the modal valuation and denote it as $V^\mathcal{M}\xspace$,
and $R$ is the accessibility relation and denote it as $R^\mathcal{M}\xspace$.
$\mathbf{Mods}$ denotes the class of all models over all domains, $\mathbf{Mods} =
\bigcup_{W} \mathbf{Mods}_W$.

Given $\mathcal{M}\xspace \in \mathbf{Mods}_{W}$, let $\mathrm{Ext}(\mathcal{M}\xspace)$, the \emph{extension of
  $\mathcal{M}\xspace$}, be the smallest subset of $\mathbf{Mods}_{W}$ that contains $\mathcal{M}\xspace$
and is such that if $\mathcal{N} \in \mathrm{Ext}(\mathcal{M}\xspace)$, then $R^{\mathcal{N}}(m,v) \subseteq
\mathrm{Ext}(\mathcal{M}\xspace)$ for all $m \in \textit{Mod}$, $v \in W$.
\end{definition}

The definition of a coinductive modal model is similar to the usual
definition of a Kripke pointed model. The difference lies in the way
the accessibility relation is defined. In particular, for each $m$ and
each state $w$, $R(m,w)$ is defined as the set of (potentially
different) models accessible from $w$ through the $m$ modality. Observe
that for each $W$, $\mathbf{Mods}_{W}$ is well-defined (coinductively), and so
does $\mathbf{Mods}$, the class of all models. Our results will apply not only
to $\mathbf{Mods}$ but to many of its subclasses.  We will be interested in
classes which are \emph{closed under accessibility relations}
(\emph{closed classes} for short): $\mathcal{M}\xspace \in \mathcal{C}\xspace$ implies $\mathrm{Ext}(\mathcal{M}\xspace)
\subseteq \mathcal{C}\xspace$.  In the rest of the paper we will only consider
classes of models closed under accessibility relations.

\begin{example}
  Consider the pointed Kripke model in
  Figure~\ref{fig:model-diff}a, and its equivalent coinductive modal model in
  Figure~\ref{fig:model-diff}b. The point of evaluation in each model is circled.
The main difference is that the relation of a coinductive model leads to another
coinductive model, whereas in a Kripke model the relation leads
to another point of the same model.

\begin{figure}[ht]
  \begin{center}
    \begin{minipage}[ht]{.35\linewidth}
      \begin{center}
        \includegraphics[scale=0.6,keepaspectratio=true]{images/kripke}

        (a)
      \end{center}
    \end{minipage}

    \begin{minipage}[ht]{.55\linewidth}
      \begin{center}
        \includegraphics[scale=0.6,keepaspectratio=true]{images/coind}

        (b)
      \end{center}
    \end{minipage}
  \end{center}
  \caption{a) A Kripke model. b) Equivalent coinductive  model.  \label{fig:model-diff}}
\end{figure}

\end{example}

We are now ready to introduce the definition of the satisfiability
relation $\models$.

\begin{definition}[Semantics]\label{def:sem}
  Let $\varphi$ be a formula in modal CNF and $\mathcal{M}\xspace = \tup{w,W,V,R}$ a model in
  $\mathbf{Mods}$. We define $\models$ for modal CNF formulas, clauses and literals
  as
  \begin{center}
    \begin{tabular}{lll}
      $\mathcal{M}\xspace \models \varphi$ &  \mbox{ iff }
      & for all clauses $C \in \varphi$ we have $\mathcal{M}\xspace \models C$\\
      $\mathcal{M}\xspace \models C$ &  \mbox{ iff }
      &  there is some literal $l \in C$ such that $\mathcal{M}\xspace \models l$\\
      $\mathcal{M}\xspace \models a$ & \mbox{ iff } & $a \in V(w)$ \mbox{ for } $a \in \textsf{Atom}\xspace$\\
      $\mathcal{M}\xspace \models \neg a$ & \mbox{ iff } & $a \not \in V(w)$ \mbox{ for } $a \in \textsf{Atom}\xspace$\\
      $\mathcal{M}\xspace \models \boxr{m} C$ &  \mbox{ iff } & $\mathcal{M}\xspace' \models C$, for all $\mathcal{M}\xspace' \in R(m,w)$\\
      $\mathcal{M}\xspace \models \neg \boxr{m} C$ &  \mbox{ iff } & $\mathcal{M}\xspace \not \models \boxr{m}C$.
    \end{tabular}
  \end{center}

\noindent
For $\mathcal{C}\xspace$ a class of models, we write $\mathcal{C}\xspace \models \varphi$ whenever
$\mathcal{M}\xspace \models \varphi$ for every $\mathcal{M}\xspace$ in $\mathcal{C}\xspace$, and we say that
$\Gamma_{\mathcal{C}\xspace} = \cset{\varphi \mid \mathcal{C}\xspace \models \varphi}$ is the
\emph{logic} defined by $\mathcal{C}\xspace$.

The set of models in $\mathcal{C}\xspace$ of a formula $\varphi$ is the set $\textit{Mod}_\mathcal{C}\xspace(\varphi)
=\csetsc{\mathcal{M}\xspace}{\mathcal{M}\xspace \in \mathcal{C}\xspace \mbox{ and } \mathcal{M}\xspace \models \varphi}$ (when
$\mathcal{C}\xspace$ is clear from the context we will just write $\textit{Mod}(\varphi)$).  We
say that $\psi$ \emph{can be inferred from} $\varphi$ in $\mathcal{C}\xspace$ and
write $\varphi \models_\mathcal{C}\xspace \psi$ if $\textit{Mod}_\mathcal{C}\xspace(\varphi) \subseteq
\textit{Mod}_\mathcal{C}\xspace(\psi)$.
\end{definition}

As shown in~\cite{arec:coin10}, the logic $\Gamma_\mathbf{Mods}$ (generated by
the class of all possible models) coincides with the basic multi-modal
logic \textsf{K}.  By properly restricting the model class we can
capture different modal logics.  Let us call a predicate $P$ on models
a \emph{defining condition} for a class $\mathcal{C}\xspace$ whenever $\mathcal{C}\xspace$ is  such
that $\mathcal{M}\xspace \in \mathcal{C}\xspace$ if and only if $P(\mathcal{M}\xspace)$
holds.  Consider the signature $\mathcal{S}\xspace = \tup{\textsf{Atom}\xspace, \textit{Mod}}$ where $\textsf{Atom}\xspace
= \textsf{Prop}\xspace \cup \textsf{Nom}\xspace$, $\textit{Mod} = \textsf{Rel}\xspace \cup \cset{\mathsf{A}} \cup \csetsc{@_i}{i
  \in \textsf{Nom}\xspace}$; and $\textsf{Prop}\xspace = \cset{p_1,p_2,\ldots}$, $\textsf{Nom}\xspace =
\cset{n_1,n_2,\ldots}$ and $\textsf{Rel}\xspace = \cset{r_1,r_2,\ldots}$ are mutually
disjoint, countable infinite sets. In what follows, we will usually be
interested in sub-languages of the language defined over $\mathcal{S}\xspace$ by
Definition~\ref{modalformula}.

\begin{figure}[ht]
  \begin{center}
    \begin{tabular}{|c|l@{\ }c@{\ }l@{\ }c@{\ }l|} \hline

      Class & \multicolumn{5}{l|}{Defining condition} \\ \hline

      $\mathcal{C}\xspace_m^\textsf{K}$ & $\mathcal{P}\xspace_{m}^{\textsf{K}}(\mathcal{M}\xspace)$ & $\Longleftrightarrow$ &
      $R^{\mathcal{M}\xspace}(m,w)$ & $\subseteq$ & $\cset{\tup{v,|\mathcal{M}\xspace|,V^{\mathcal{M}\xspace},R^{\mathcal{M}\xspace}} \mid v \in |\mathcal{M}\xspace|}, m \in \textsf{Rel}\xspace$  \\ \hline

      $\mathcal{C}\xspace_{\mathsf{A}}$ & $\mathcal{P}\xspace_\mathsf{A}(\mathcal{M}\xspace)$ & $\Longleftrightarrow$ &
      $R^{\mathcal{M}\xspace}(\mathsf{A}, w)$  &  = & $\cset{\tup{v, |\mathcal{M}\xspace|,V^{\mathcal{M}\xspace}, R^{\mathcal{M}\xspace}} \mid v \in |\mathcal{M}\xspace|}$\\ \hline

      $\mathcal{C}\xspace_{@_i}$ & $\mathcal{P}\xspace_{@_i}(\mathcal{M}\xspace)$ & $\Longleftrightarrow$ &
      $R^{\mathcal{M}\xspace}(@_i,w)$ & = & $\cset{\tup{v,|\mathcal{M}\xspace|,V^{\mathcal{M}\xspace},R^{\mathcal{M}\xspace}} \mid i \in V(v)},  i \in \textsf{Nom}\xspace$\\\hline
      $\mathcal{C}\xspace_{\mbox{\tiny \textsf{Nom}\xspace}}$ & $\mathcal{P}\xspace_{\mbox{\tiny \textsf{Nom}\xspace}}(\mathcal{M}\xspace)$ & $\Longleftrightarrow$ &
      \multicolumn{3}{@{}l|}{$\{w \mid i \in V^{\mathcal{M}\xspace}(w)$\} is a singleton, $\forall i \in \textsf{Nom}\xspace$} \\ \hline
    \end{tabular}
  \end{center}
  \vspace*{-.3cm}
  \caption{Defining conditions for different modal
    logics}\label{fig:classes}
\end{figure}

Figure~\ref{fig:classes} introduces a number of closed model classes
by means of their defining conditions. Observe that $\mathcal{P}\xspace_{m}^{\textsf{K}}$ is
true for a model $\mathcal{M}\xspace$ if every successor of $w^{\mathcal{M}\xspace}$ is identical to
$\mathcal{M}\xspace$ except perhaps on its point of evaluation. We call $m$ a
\emph{relational modality} when it is interpreted in $\mathcal{C}\xspace_{m}^{\textsf{K}}$
because over this class they behave as classical relational
modalities~\cite{arec:coin10}.

We can capture different modal operators, like the ones from hybrid
logics~\cite{arec:hybr05b}, by choosing the proper class of models.
Predicates $\mathcal{P}\xspace_\mathsf{A}$ and $\mathcal{P}\xspace_{@_i}$, for instance, impose conditions
on the point of evaluation of the accessible models restricting the evaluation
to the class of models where the relation is, respectively, the total
relation ($\forall x y . R(x,y)$) and the `point to all $i$' relation
($\forall x y . R(x,y) \leftrightarrow i(y)$). Observe that whenever the atom
$i$ is interpreted as a singleton set, the `point to all $i$' relation
becomes the usual `point to $i$' relation ($\forall x y . R(x,y) \leftrightarrow
y = i$) of hybrid logics.  Finally, predicate $\mathcal{P}\xspace_{\textsf{Nom}\xspace}$ turns
elements of $\textsf{Nom}\xspace$ into nominals, i.e., true at a unique element of
the domain of the model.

An interesting feature of this setting is that we can express the
combination of modalities as the intersection of their respective
classes.  For example, $\mathcal{C}\xspace_{\mathcal{H}\xspace(@)}$, the class of models for the
hybrid logic $\mathcal{H}\xspace(@)$, can be defined as follows:
$$
\begin{array}{c}
  \mathcal{C}\xspace_{\mathcal{H}\xspace(@)}  =  \mathcal{C}\xspace_{\textsf{Nom}\xspace} \cap \mathcal{C}\xspace_@  \cap \mathcal{C}\xspace_{\textsf{Rel}\xspace}\mbox{, where }\\
  \mathcal{C}\xspace_{@}   =  \bigcap_{i \in \textsf{Nom}\xspace}\mathcal{C}\xspace_{@_i} \mbox{, and }
  \mathcal{C}\xspace_{\textsf{Rel}\xspace}  =  \bigcap_{m \in \textsf{Rel}\xspace}\mathcal{C}\xspace^{\textsf{K}}_{m}.
\end{array}
$$

The crucial characteristic of the coinductive approach is that all these
different modal operators are captured using the same semantic condition
introduced in Definition~\ref{def:sem}. All the details defining each
particular operator are now introduced as properties of the accessibility
relation. As a result, a unique notion of bisimulation is sufficient to
cover all of them.

\begin{definition}[Bisimulations]\label{def:bisim}
  Given two models $\mathcal{M}\xspace$ and $\mathcal{M}\xspace'$ we say that \emph{$\mathcal{M}\xspace$ and $\mathcal{M}\xspace'$
    are bisimilar} (notation $\mathcal{M}\xspace \mathop{\underline{\leftrightarrow}} \mathcal{M}\xspace'$) if $\mathcal{M}\xspace \mathop{Z}
  \mathcal{M}\xspace'$ for some relation $Z \subseteq \mathrm{Ext}(\mathcal{M}\xspace) \times \mathrm{Ext}(\mathcal{M}\xspace')$
  such that whenever $\tup{w,W,V,R} \mathop{Z}$ $\tup{w',W',V',R'}$ we
  have the following properties:
  \begin{itemize}
  \item \textbf{Harmony:} $a \in V(w)$ iff $a \in V'(w')$, for all $a
    \in \textsf{Atom}\xspace$.
  \item \textbf{Zig:} $\mathcal{N} \in R(m,w)$ implies $\mathcal{N} \mathop{Z} \mathcal{N}'$
    for some $\mathcal{N}' \in R'(m,w')$.

  \item \textbf{Zag:}$\mathcal{N}' \in R'(m,w')$ implies $\mathcal{N} \mathop{Z} \mathcal{N}'$
    for some $\mathcal{N} \in R(m,w)$.
  \end{itemize}
  Such $Z$ is called a \emph{bisimulation between $\mathcal{M}\xspace$ and $\mathcal{M}\xspace'$}.
\end{definition}

The classic result of invariance of modal formulas under
bisimulation~\cite{MLBOOK} can easily be proved.

\begin{theorem}\label{invariance}
  If $\mathcal{M}\xspace \mathop{\underline{\leftrightarrow}} \mathcal{M}\xspace'$, then $\mathcal{M}\xspace \models \varphi$ iff $\mathcal{M}\xspace' \models
  \varphi$, for all $\varphi$.
\end{theorem}

As stated in~\cite{arec:coin10},  this
general notion of bisimulation works for every modal logic definable
as a closed subclass of $\mathbf{Mods}$.

\section{Symmetry Detection} \label{sec:detection}

Different techniques have been proposed for detecting symmetries of
propositional formulas in clausal form. Some of them, deal directly
with the formula~\cite{Benhamou:1994tr}, while others, reduce the
problem to the problem of finding automorphisms in colored graphs
constructed in such a way that the automorphism group of the graph is
isomorphic to the symmetry group of the formula under
consideration~\cite{Crawford:1992wz,Crawford:1996wa,Aloul:2002ww}.

The availability of efficient tools to detect graph automorphisms
(e.g.,~\cite{McKay:1990vf,Darga:2004us,Junttila:2007vx}) has made the
later approach the most successful one because it is fast and easy to
integrate.

In this section we present a technique for the detection of symmetries
in modal formulas that extends the construction proposed for
propositional formulas to modal CNF
formulas. We present the graph construction algorithm and prove its
correctness.

We now introduce some notation and definitions.  In what follows, we
consider modal CNF formulas as set of sets as defined in Section~\ref{sec:defs} and write $\psi \in \varphi$ to express that
$\psi$ is subformula  of $\varphi$. Clauses occurring at modal depth 0 are named \emph{top
  clauses} and clauses occurring in modal literals are named
\emph{modal clauses}.
Let $s:\textit{Mod} \times \{0,1\} \mapsto \mathbb{N}\backslash \{0,1\}$ be an
injective function and let $t: Sub(\varphi) \mapsto \mathbb{N}$ be a
partial function defined as:
$$
t(\psi) = \left \{
  \begin{array}{lll}
    1 & \mbox{if } \psi \mbox{ is a top clause } \\
    s(m,0) & \mbox{if } \psi = \boxr{m}C \\
    s(m,1) & \mbox{if } \psi = \neg \boxr{m}C
  \end{array}
\right.
$$

\noindent
The \emph{typing} function $t$ assigns a numeric type to every clause
(top or modal). For modal clauses, the type is based on the modality
and the polarity of the modal literal in which it occurs.
Let us assign to each clause $C$ occurring in $\varphi$ a unique identifier $\mathit{id}(C)={\tup{m, k, i}}$ where $m$ is the modal depth at which the clause occurs, $k=t(\psi)$ is the type of the clause as returned by the
\emph{typing} function $t$ and $i \in \mathbb{N}$ is different for each clause. To
simplify notation, in what follows we will assume that each clause $C$ is labeled by
its unique identifier $\mathit{id}(C)={\tup{m, k, i}}$ and write $C_{m,k,i}$.

By definition, a symmetry of a formula $\varphi$ is a bijective function that maps
literals to literals. It can naturally be extended to a function $\sigma_{ext}$ that also maps
each clause $C$ to $\sigma(C)$.  Notice that because
$\sigma$ is a symmetry of $\varphi$ both $C$ and $\sigma(C)$ are clauses in $\varphi$.
Hence, both $C$ and $\sigma(C)$ will be assigned some identifier by the $\mathit{id}$ function.

The following are properties of $\sigma_{ext}$ that are easy to verify.

\begin{proposition}\label{prop:sext}
  Let $\varphi$ be a modal CNF formula and $\sigma$ a symmetry of
  $\varphi$. Then for the extension of $\sigma$, $\sigma_{ext}$, the
  following holds:
  \begin{enumerate}[label=\emph{\roman*})]
  \item\label{sext:1} $\sigma_{ext}$ is a bijective function.
  \item\label{sext:3} If $\sigma_{ext}(C_{m,k,i}) = C_{m',k',i'}$ then $m=m'$.
  \item\label{sext:4} If $\sigma_{ext}(C_{m,k,i}) = C_{m',k',i'}$ then $k=k'$.
  \item\label{sext:5} If $l \in C_{m,k,i}$ then $\sigma_{ext}(l) \in \sigma_{ext}(C_{m,k,i})$.
  \item\label{sext:2} $\sigma_{ext}$ is a symmetry of $\varphi$.

  \end{enumerate}
\end{proposition}

\newcommand{G(\varphi)}{G(\varphi)}

We can now introduce the construction of the colored graph corresponding
to a given formula $\varphi$. We will construct an undirected colored graph
with two types of edges.
As coloring function we will use the typing
function $t$ introduced earlier in this section.

\begin{definition}\label{def:graph}
  Let $\varphi$ be a modal CNF formula and let $At(\varphi)$ denote
  the set of atoms occurring in $\varphi$. The colored graph
  $G(\varphi)=(V,E_{1},E_{2})$ is constructed as follows:

  \begin{enumerate}
  \item For each atom $a \in At(\varphi)$:

    \begin{enumerate}
    \item Add two \emph{literal} nodes of color 0: one labelled $a$
      and one labelled $\neg a$.

    \item Add an edge to $E_{1}$ between these two nodes to ensure Boolean
      consistency.
    \end{enumerate}

   \item For each top clause $C$ of $\varphi$ add a \emph{clause} node of
     color $t(C)$.

   \item \label{cons:point2} For each atom literal occurring in $C$,
     add an edge to $E_{1}$ from $C$ to the corresponding literal node.

  \item For each modal literal $\boxr{m}C'$ ($\neg \boxr{m}C'$) occurring in $C$:
    \begin{enumerate}
    \item Add a clause node of color $t(\boxr{m}C')$
      ($t(\neg\boxr{m}C')$) to represent the modal clause $C'$.

    \item Add an edge to $E_{1}$ from the node of $C$ to this node.
    \item If $m$ is indexed by an atom literal $l$ then add an edge to $E_{2}$
      from the node $C'$ to the indexing literal $l$.

    \item Repeat the process from point \ref{cons:point2} for each
      literal (atom or modal) occurring in $C'$.
    \end{enumerate}

  \end{enumerate}

\end{definition}

This construction creates a graph with $2 + 2|\textit{Mod}|$ colours and at
most $(2|V| +\#(\mbox{TopClauses}) + \#(\mbox{ModalClauses}))$ nodes.

\begin{example}
  Let us consider the following  formula $\varphi = (a \vee \boxr{m}(b
  \vee \neg \boxr{m}c)) \wedge (b \vee \boxr{m}(a  \vee \neg \boxr{m}c))$.
  This formula has six clauses (2 at modal depth 0, 2 at modal depth 1
  and 2 at modal depth 2) and three atoms (six literals).  The
  associated colored graph, $G(\varphi)$, is shown in Figure~\ref{fig:graph1}
  (colors are represented by shapes in the figure).

  \begin{figure}[ht]
    \begin{center}
      \begin{tabular}{ll}
        \begin{picture}(200,0)
          \put(0,-50){\includegraphics[scale=0.5,keepaspectratio=true]{images/graph1}}
        \end{picture}
        &

        $\begin{array}{l}
          A =  (a \vee \boxr{m}(b \vee \neg \boxr{m}c))\\
          B =  (b \vee \boxr{m}(a \vee \neg \boxr{m}c))\\
          C = \boxr{m}(b \vee \neg \boxr{m}c)\\
          D = \boxr{m}(a \vee \neg \boxr{m}c) \\
          E = \boxr{m}c \\
          F = \boxr{m}c\\
        \end{array}$
      \end{tabular}
    \end{center}
    \caption{Graph representation of $\varphi$.}\label{fig:graph1}
  \end{figure}

\end{example}

Note that the construction of Definition~\ref{def:graph} induces a
mapping $g$ that associates to each literal and clause the
corresponding node in the graph.

To prove that the proposed construction is correct, we first have to
show that each symmetry of the formula is a colored automorphism of
the graph.

\begin{proposition}\label{prop:sym2graph}
  Let $\varphi$ be a modal CNF formula, $\sigma$ a symmetry of
  $\varphi$, $G(\varphi)=(V,E_1,E_2)$ the colored graph of $\varphi$ as
  defined by Definition \ref{def:graph}, and $g$ the mapping induced
  by the construction of $G(\varphi)$. Then $\pi= g \circ \sigma_{ext}$ is an
  automorphism of $G(\varphi)$.
\end{proposition}

\begin{proof}
To simplify notation lets assume that $g$ is
the identity function (i.e., we do not differentiate between a clause
(or literal) and its associated node in the graph) and as a consequence $\pi = \sigma_{ext}$.
Then $\pi$ is an automorphism of  $G(\varphi)$ if the following holds:

\begin{enumerate}

\item \label{aut:1}$(l,\neg l) \in E_{1}$
  iff $(\pi(l),\pi(\neg l)) \in E_{1}$ for all $l \in V$.

  We have to consider the following cases:
  \begin{itemize}
    \setlength{\itemsep}{5pt}
  \item[-] $\sigma$ is a permutational symmetry: \\
    \underline{($\rightarrow$):}
    Assume $\pi=\sigma_{ext}=(a \ b)(\neg a\ \neg
    b)$. Then $(\pi(a),\pi(\neg a)) = (b,\neg b) \in E_1$
    by construction of $G(\varphi)$.

    \underline{($\leftarrow$):} $(a,\neg a) \in E_1$ by construction of $G(\varphi)$.

  \item[-] $\sigma$ is a phase-shift symmetry:\\
    \underline{($\rightarrow$):} Assume $\pi=\sigma_{ext}=(a \ \neg
    a)$. Then $(\pi(a),\pi(\neg a)) = (\neg a, a)$, but given
    that $G(\varphi)$ is an undirected graph $(\neg a, a) = (a,\neg a) \in
    E_{1}$ by construction.

    \underline{($\leftarrow$):} $(a,\neg a) \in E_{1}$ by construction of $G(\varphi)$.

  \item[-] $\sigma$ is a compositional symmetry: It follows
    directly from the previous two cases.
 \end{itemize}

\item \label{aut:2}$(l, C_{m,k,i}) \in E_{1}$ iff $(\pi(l),
  \pi(C_{m,k,i})) \in E_{1}$ for all $l, C_{m,k,i} \in V$.

\underline{($\rightarrow$):} By construction, $(l, C_{m,k,i}) \in E_{1}$ only
if $l \in C_{m,k,i}$. Then, given that $\sigma_{ext}$ is a symmetry and
by Proposition \ref{prop:sext}\ref{sext:5}, we
know that $\sigma_{ext}(l)$ and $\sigma_{ext}(C_{m,k,i})$ both occur in $\varphi$ and
$\sigma_{ext}(l) \in \sigma_{ext}(C_{m,k,i})$. Then, by construction, we have
that $(\pi(l), \pi(C_{m,k,i})) \in E_{1}$.

\underline{($\leftarrow$):} It follows directly by construction of
$G(\varphi)$.

\item \label{aut:3}$(C_{m,k,i},C_{m',k',i'}) \in E_{1}$ iff
  $(\pi(C_{m,k,i}),\pi(C_{m',k',i'})) \in
  E_{1}$ for all $C_{m,k,i},C_{m',k',i'} \in V$.

  \underline{($\rightarrow$):} If $(C_{m,k,i},C_{m',k',i'}) \in E_{1}$ we
  know that either $m < m'$ or $m > m'$. Assume $m < m'$ then
  $C_{m',k',i'}$ is a modal clause occurring in $C_{m,k,i}$. By
  Proposition \ref{prop:sext}\ref{sext:5}, we have that
  $\sigma_{ext}(C_{m',k',i'})$ is a modal clause occurring in
  $\sigma_{ext}(C_{m,k,i})$, and given that $\sigma_{ext}$ is a symmetry of
  $\varphi$, $\sigma_{ext}(C_{m,k,i})$ and $\sigma_{ext}(C_{m',k',i'})$ both occur
  in $\varphi$, therefore, by construction, $\pi(C_{m,k,i}) \in V$ and,
  $\pi(C_{m',k',i'}) \in V$, therefore $(\pi(C_{m,k,i}),\pi(C_{m',k',i'})) \in E_{1}$.

\underline{($\leftarrow$):} It follows directly by construction of
$G(\varphi)$.

\item \label{aut:4}$(l,C_{m,k,i}) \in E_{2}$ iff
  $(\pi(l),\pi(C_{m,k,i})) \in E_{2}$ for all $l, C_{m,k,i} \in V $.

  \underline{($\rightarrow$):} $(l,C_{m,k,i}) \in E_{2}$ if the modality
  of the modal clause $C_{m,k,i}$ is indexed by $l$. Given that $\sigma_{ext}$
  is a symmetry of $\varphi$, we know that $\sigma_{ext}(l) \in
  \varphi$ and
  $\sigma_{ext}(C_{m,k,i}) \in \varphi$ and that $\sigma_{ext}(l)$ index the
  modality of the modal clause $\sigma_{ext}(C_{m,k,i})$, therefore, by
  construction, $\pi(l) \in V$ and $\pi(C_{m,k,i}) \in V$ and
  $(\pi(l),\pi(C_{m,k,i})) \in E_{2}$.

\underline{($\leftarrow$):} It follows directly by construction of
$G(\varphi)$.

\item \label{aut:5} For every cycle $(x \
  y) \in \pi$, $x$ and $y$ have the same color.

Follows from Proposition~\ref{prop:sext}\ref{sext:4} and the fact that
by construction different types of clauses are assigned different
colors in the graph.
\end{enumerate}
\end{proof}

We now prove that any colored automorphism of $G(\varphi)$ induces a symmetry of $\varphi$.

\begin{proposition}\label{prop:graph2sym}
  Let $\varphi$ be a modal CNF formula,  $G(\varphi)=(V,E_1,E_2)$ the colored graph of $\varphi$ as defined
  by Definition \ref{def:graph}, $\pi$ an automorphism of
  $G(\varphi)$ and $g$ the mapping induced by the construction of
  $G(\varphi)$. Then $\sigma_{ext}= g^{-1} \circ \pi$ is a symmetry of
  $\varphi$.
\end{proposition}

\begin{proof}
  Once more, assume $g$ is the identity. To prove that $\sigma_{ext}$ is a symmetry of $\varphi$, we have to prove
  the following properties:

  \begin{enumerate}
  \item $\sigma_{ext}$ is a consistent permutation, i.e., $\sigma_{ext}(\neg l)
    = \neg \sigma_{ext}(l)$ for all $l \in \textsf{ALit}\xspace$.

By construction, Boolean consistency edges only connect
literal nodes. Let $l_i \in V$ be a literal node. Then by construction
we have that $(l_i, \neg l_i) \in E_1$. Now assume that $\pi(l_i)=l_j$
for $l_j \in V$. Given
that $\pi$ is an automorphism it must be the case that
$(\pi(l_i), \pi(\neg l_i)) \in E_1$, and therefore that
$\pi(\neg l_i)=\neg l_j = \neg \pi(l_i)$, which implies that
$\sigma_{ext}(\neg l_i)=\neg \sigma_{ext}(l_i)$.

\item If $C_{m,k,i} \in \varphi$ then $\sigma_{ext}(C_{m,k,i}) \in \varphi$.

  By construction $C_{m,k,i} \in V$ implies that $C_{m,k,i} \in \varphi$. As
  $\pi$ is an automorphism, $\pi(C_{m,k,i}) \in V$, therefore,
  $\pi(C_{m,k,i}) \in \varphi$ which implies that $\sigma_{ext}(C_{m,k,i}) \in \varphi$.

\item If $l \in \varphi$ then $\sigma_{ext}(l) \in \varphi$.

It follows by the same argument as in the previous case.

\item If $\sigma_{ext}(C_{m,k,i})=C_{m',k',i'}$ then $k=k'$.

It follows from the fact that $\pi$ is a colored automorphism,
mapping only nodes of the same color, and that by construction, clauses of
the same type are assigned the same color in the
graph.

\item If $\sigma_{ext}(C_{m,k,i})=C_{m',k',i'}$ then $m=m'$.

We prove this by induction on $m$, the modal depth at which a
clause occurs in $\varphi$.

\underline{Base Case: $m=0$.}
We have to prove that if $\sigma_{ext}(C_{0,k,i})=C_{m',k',i'}$ then $m'=0$.
Assume that $m'\neq 0$. Then, there is a clause $C_{n,s,j}$, with $n<m'$ such
that, $C_{m',k',i'}$ is a modal clause occurring in it. By
construction, we then have that $(C_{n,s,j},C_{m',k',i'}) \in E_{1}$. As
$\pi$ is an automorphism of $G(\varphi)$, we should have
$(\pi(C_{n,s,j}),\pi(C_{m',k',i'})) = (\pi(C_{n,s,j}),C_{0,k,i}) \in
E_{1}$, but by construction there is no such edge.

\underline{Inductive Step: $n<m \implies m$.}
By construction of $G(\varphi)$ if $(C_{m,k,i},C_{n,l,j}) \in E_{1}$ then $|m - n| = 1$.
Now, assume $m\neq m'$. We know that there is a clause
$C_{(m'-1),s,j}$ such that $(C_{(m'-1),s,j},C_{m',k',i'}) \in
E_{1}$.
Then, as $\pi$ is an automorphism of $G(\varphi)$, it must be the case that
$(\pi(C_{(m'-1),s,j}),\pi(C_{m',k',i'}))=(\pi(C_{(m'-1),s,j}),C_{m,k,i})
\in E_{1}$. By the inductive hypothesis we know that
$\pi(C_{(m'-1),s,j}) = C_{(m'-1),s,j'}$ and therefore, we have that
$(C_{(m'-1),s,j'},C_{m,k,i}) \in E_{1}$. But then we get that $|m -
(m'-1)| \geq 2$, which by construction cannot happen. Therefore
 $(C_{(m'-1),s,j'},C_{m,k,i}) \not \in E_{1}$,
contradicting the fact that $\pi$ is an automorphism of $G(\varphi)$.

\item If $l$ index a clause $C_{m,k,i}$ then $\sigma_{ext}(l)$ index the
  clause $\sigma_{ext}(C_{m,k,i})$.

If $l$ index a clause $C_{m,k,i}$, then by construction $(l,C_{m,k,i}) \in
E_2$. Given that $\pi$ is an automorphism, $(\pi(l),\pi(C_{m,k,i})) \in
E_2$, which implies that $\sigma_{ext}(l)$ index the
  clause $\sigma_{ext}(C_{m,k,i})$.
  \end{enumerate}
We have proved that $\sigma_{ext}$, the extension of $\sigma$, obtained
from an automorphism of the graph, is a symmetry of $\varphi$. To obtain
the original symmetry $\sigma$ we just take the restriction of $\sigma_{ext}$ to
atom literals.
\end{proof}

Finally we can prove that our construction is correct.
\begin{theorem}
  Let $\varphi$ be a modal CNF formula and $G(\varphi)= (V,E_{1},E_{2})$ the
  colored graph constructed following the construction of Definition
  \ref{def:graph}. Then every symmetry $\sigma$ of $\varphi$
  corresponds one-to-one to an automorphism $\pi$ of
  $G(\varphi)$.
\end{theorem}
\begin{proof}
Immediate from Proposition~\ref{prop:sym2graph} and~\ref{prop:graph2sym}.
\end{proof}

This construction enables the detection of symmetries as defined
in Section~\ref{sec:lit-symm},
that is, symmetries defined over literals that can appear at various
modal depths of a given formula.
To detect layered symmetries (see Section~\ref{sec:layering}) for logics with the tree model closure
property,  the construction needs to be
modified to capture the notion of layers. This is easy to achieve by just
changing the way literals occurring in the formula are handled
(see~\cite{orbe2012} for details). Properties~\ref{prop:sym2graph} and~\ref{prop:graph2sym}
(suitably generalized) also hold in this case.

\section{Symmetries in Automated Theorem Proving}\label{sec:intro}

Many concrete, real life problems present symmetries.  For instance,
if we want to know whether trying to place three pigeons in two
pigeonholes results in two occupying the same nest, it does not really
matter which of all pigeons gets in each pigeonhole.  Starting by
putting the first pigeon to the first pigeonhole is the same as if we
put the second one in it.  In mathematical and common-sense reasoning
these kinds of symmetries are often used to reduce the difficulty of
reasoning --- one can analyze in detail only one of the symmetric
cases and generalize the result to the others.  The exact same is done
in propositional theorem proving. Many problem classes and, in
particular, those arising from real world applications, display a
large number of symmetries; and current SAT solvers take into account
these symmetries to avoid exploring duplicate branches of the search
space. In the last years there has been extensive research in this
area, focusing on how to define symmetries, how to detect them
efficiently, and how SAT solvers can better profit from
them~\cite{Prasad05asurvey}.

Informally, we can define a symmetry of a discrete object as a
permutation of its components that leaves the object, or some aspect
of it, intact (think of the rotations of a spatial solid).  In the context
of SAT solving we can formally define a symmetry as a permutation of
the variables (or literals) of a problem that preserves its
structure and, in particular, its set of solutions.  Depending on
which aspect of the problem is kept invariant, symmetries are
classified in the literature into semantic or
syntactic~\cite{Benhamou:1992vx}.  Semantic symmetries are intrinsic
properties of a Boolean function that are independent of any
particular representation, i.e., a permutation of variables that does
not change the value of the function under any variable
assignment. Syntactic symmetries, on the other hand, correspond to the
specific algebraic representation of the function, i.e., a permutation
of variables or literals that does not change the representation. A
syntactic symmetry is also a semantic symmetry, but the converse does
not always hold.

In~\cite{Krishnamurthy:1985ug}, Krishnamurthy used symmetries in the
context of SAT solving. In this article, the notions of \emph{global}
and \emph{local} symmetries as inference rules are used to strengthen
resolution-based proof systems for propositional logic, showing that
they can shorten the proofs of certain difficult propositional
problems like the pigeonhole principle. Since then, many articles discuss how to detect and exploit symmetries. Most of them can be
grouped into two different approaches: static symmetry breaking and
dynamic symmetry breaking.  In the first
approach~\cite{Crawford:1992wz,Crawford:1996wa,Aloul:2002ww},
symmetries are detected and eliminated from the problem statement
before the SAT solver is used. They work as a preprocessing step.  In
contrast, dynamic symmetry breaking~\cite{Brown:1989uw,Benhamou:1992vx,Benhamou:1994tr} detects
and breaks symmetries during the search space exploration.  The first
approach can be used with any theorem prover; the second is prover
dependent but it can take
advantage of symmetries that emerge during search.
Despite their differences they share the same goal: to identify
symmetric branches of the search space and guide the SAT solver away
from symmetric branches already explored.  A third alternative was
introduced in~\cite{Benhamou:uv}, which combines symmetry reasoning
with clause learning~\cite{ryan} in Conflict-Driven Clause Learning
SAT solvers~\cite{Een:2004uh}. The idea is to augment clause
learning by using the symmetries of the problem to learn the
symmetric equivalents of conflict-induced clauses. This approach is
particularly appealing as it does not imply major modifications
to the search procedure and the required modifications to the clause
learning process are minor.

Symmetries have been extensively investigated and successfully
exploited for propositional logic SAT and some results involve other
logics, see~\cite{Audemard:2002ti,Audemard:2004up,fontaine2011}.  To the best
of our knowledge, symmetries remain largely unexplored in automated
theorem proving for modal logics.

In this paper, we generalize the notion of symmetries to modal formulas in
conjunctive normal form for different modal logics including the basic
modal language over different model classes (e.g., reflexive, linear
or transitive models), and logics with additional modal operators
(e.g., universal and hybrid operators).  The main result of the
article shows that symmetries of a modal formula preserve entailment:
if $\sigma$ is a symmetry of $\varphi$ then $\varphi \models \psi$ if
and only if $\varphi \models \sigma(\psi)$.  In cases where the modal
language has a tree model
property, we can actually use a more flexible notion of symmetry that
enables different permutations to be applied at each modal depth.
We also present a method to detect the symmetries of modal
formulas in conjunctive normal form. This method reduces the symmetry
detection problem to the graph automorphism problem. A  general graph
construction algorithm, suitable for many modal logics, is presented.
In order to tackle a broad range of modal languages that may or may not enjoy
the tree model property, we use in our work  the semantics provided by
coinductive modal models~\cite{arec:coin10} instead of the more familiar Kripke relational
semantics. Coinductive modal models provide a homogeneous framework
to investigate different modal languages at a greater level of
abstraction. A consequence of this is that results obtained in the
coinductive framework can be easily extended to concrete modal
languages by just giving the appropriate definition of the model
classes and fixing some parameters.

In Section~\ref{sec:defs} we present modal logics and coinductive
modal models.  In Section~\ref{sec:lit-symm} we define modal
symmetries, together with the appropriate notion of simulation to show
that symmetries preserve modal entailment.  In
Section~\ref{sec:layering} we introduce layered permutations and show
that they can be used when the modal logic has the adequate notion of
the tree model property. In Section \ref{sec:detection} we present a
graph construction algorithm to detect symmetries in modal formulas
and prove its correctness. We draw our conclusions and discuss future
research in Section~\ref{sec:conclusion}.

\section{Layered Permutations} \label{sec:layering}

In this section we
present the notion of layered permutations. First, we
present a definition of the tree model property~\cite{MLBOOK}
for coinductive modal models that we will use.

Given a model $\mathcal{M} = \langle W,R,V \rangle$, a (finite) \emph{path rooted at $\mathcal{M} = \langle W,R,V \rangle$} is a
sequence $\pi=(\mathcal{M} = \langle W,R,V \rangle_0,m_{1},\mathcal{M} = \langle W,R,V \rangle_{1},\ldots,m_{k},\mathcal{M} = \langle W,R,V \rangle_{k})$, for $m_i \in
\textit{Mod}$ where $\mathcal{M} = \langle W,R,V \rangle_0 = \mathcal{M} = \langle W,R,V \rangle$, $k \ge 0$, and $\mathcal{M} = \langle W,R,V \rangle_{i} \in
R(m_{i},w^{\mathcal{M} = \langle W,R,V \rangle_{i-1}})$ for $i=1,\ldots,k$. For a path
$\pi=(\mathcal{M} = \langle W,R,V \rangle_0,m_{1},\mathcal{M} = \langle W,R,V \rangle_{1},\ldots,m_{k},$ $\mathcal{M} = \langle W,R,V \rangle_{k})$ we define $\textit{first}(\pi) =
\mathcal{M} = \langle W,R,V \rangle_0$, $\textit{last}(\pi) = \mathcal{M} = \langle W,R,V \rangle_k$, and $\textit{length}(\pi) = k$.  We denote the set
of all paths rooted at $\mathcal{M} = \langle W,R,V \rangle$ as $\Pi[\mathcal{M} = \langle W,R,V \rangle]$. A coinductive tree model is a model that has a unique path to every
reachable model (every model in $\mathrm{Ext}(\mathcal{M} = \langle W,R,V \rangle)$).  Formally we can define
the class of all coinductive tree models, $\mathcal{C}\xspace_{Tree}$, with the
following defining condition:
$$
\mathcal{C}\xspace_{\textit{Tree}}:= P_{\textit{Tree}}(\mathcal{M} = \langle W,R,V \rangle) \Longleftrightarrow \textit{last}:\Pi[\mathcal{M} = \langle W,R,V \rangle] \mapsto
\mathrm{Ext}(\mathcal{M} = \langle W,R,V \rangle) \mbox{ is bijective.}
$$

For example, the \emph{unravelling} construction (in its version for
coinductive modal models) shown below always defines a model in $\mathcal{C}\xspace_{Tree}$.

\begin{definition}[Model Unravelling]
  Given a model $\mathcal{M} = \langle W,R,V \rangle=\tup{w,W,V,R}$, the \emph{unravelling} of $\mathcal{M} = \langle W,R,V \rangle$, (notation
  $\mathcal{T}(\mathcal{M} = \langle W,R,V \rangle)$), is the rooted coinductive model $\mathcal{T}(\mathcal{M} = \langle W,R,V \rangle) = \langle
  (\mathcal{M} = \langle W,R,V \rangle),\Pi[\mathcal{M} = \langle W,R,V \rangle],V',R'\rangle$ where
$$
\begin{array}{rcll}
  V'(\pi)  & = & V(w^{\textit{last}(\pi)}), \mbox{ for all } \pi \in \Pi[\mathcal{M} = \langle W,R,V \rangle],\\
  R'(m, \pi)& = & \{ \tup{\pi', \Pi[\mathcal{M} = \langle W,R,V \rangle],V',R'} \mid \textit{last}(\pi') \in
  R(m,\textit{last}(\pi))\},   & \mbox{for }m \in \textit{Mod}, \pi \in \Pi[\mathcal{M} = \langle W,R,V \rangle].
\end{array}
$$
\end{definition}

It is easy to verify that given a model $\mathcal{M} = \langle W,R,V \rangle$, its unravelling $\mathcal{T}(\mathcal{M} = \langle W,R,V \rangle)$
is a tree ($\mathcal{T}(\mathcal{M} = \langle W,R,V \rangle) \in \mathcal{C}\xspace_{Tree}$) and, as expected, $\mathcal{M} = \langle W,R,V \rangle$ and
$\mathcal{T}(\mathcal{M} = \langle W,R,V \rangle)$ are bisimilar.

In what follows, we will use trees to define a more flexible family of
symmetries that we call \emph{layered symmetries}.  The following will
give a sufficient condition ensuring that layered symmetries also
preserve entailment.

\begin{definition}[Tree model closure property]\label{def:tree}
  We say that a class $\mathcal{C}\xspace$ of models is \emph{closed under trees} if
  for every model $\mathcal{M} = \langle W,R,V \rangle \in \mathcal{C}\xspace$ there is a tree model $\mathcal{T} \in \mathcal{C}\xspace$ such
  that $\mathcal{M} = \langle W,R,V \rangle \mathop{\underline{\leftrightarrow}} \mathcal{T}$.
\end{definition}

\noindent
From this definition, it follows that a class of models $\mathcal{C}\xspace$ closed
under unravellings ($\mathcal{T}(\mathcal{M} = \langle W,R,V \rangle) \in \mathcal{C}\xspace$ for all $\mathcal{M} = \langle W,R,V \rangle \in \mathcal{C}\xspace$) is also
closed under trees.

\begin{example}
  Trivially the class $\mathbf{Mods}$ (i.e., the basic modal logic) is closed
  under trees, and so does the class
  $\mathcal{C}\xspace_{\textsf{KAlt}_1}$ of models where the
  accessibility relation is a partial function.  Many classes like
  $\mathcal{C}\xspace_\mathsf{A}$, $\mathcal{C}\xspace_{@_i}$ and $\mathcal{C}\xspace_\textsf{Nom}\xspace$ fail to be closed under trees.
\end{example}

Logics defined over classes closed under trees have an interesting
property: there is a direct
correlation between the syntactical modal depth of the formula and the
depth in a tree model satisfying it.  In tree models, a notion of
layer is induced by the depth (distance from the root) of the nodes in
the model. Similarly, in modal formulas,  a notion of layer is induced
by the nesting of the modal operators.  A consequence of this
correspondence is that literals occurring at different formula layers
are semantically independent of each other (see~\cite{arec:tree00} for
further discussion), i.e., at different layers the same literal can be
assigned a different value.

\begin{example}
Consider  the formula $\varphi = (p \vee q) \wedge (r \vee \neg \Box
(\neg p \vee q \vee \Box \neg r))$ and a tree model $\mathcal{M} = \langle W,R,V \rangle$ of $\varphi$. Figure \ref{fig:layering} shows the layers induced by the
modal depth of the formula and the corresponding depth in $\mathcal{M} = \langle W,R,V \rangle$.
\begin{figure}[h]
  \begin{center}
    \includegraphics[scale=0.6,keepaspectratio=true]{images/layering}
  \end{center}
  \vspace*{-.3cm}
  \caption{Induced layering on a model and a formula.}\label{fig:layering}
\end{figure}

\end{example}

The independence between literals at different layers enables us to give a more flexible notion of
a permutation that we will call \emph{layered permutation}.
Key to the notion of layered permutation is that of a \emph{permutation sequence}.

\begin{definition}[Permutation Sequence]
  We define a finite permutation sequence $\bar{\sigma}$ as either
  $\bar{\sigma} = \tup{}$ (i.e., $\bar{\sigma}$ is the empty sequence)
  or $\bar{\sigma} = \sigma:\bar{\sigma}_2$ with $\sigma$ a
  permutation and $\bar{\sigma}_2$ a permutation sequence.
  Alternatively we can use the notation $\bar{\sigma} = \tup{\sigma_1,
    \ldots, \sigma_n}$ instead of $\bar{\sigma} =
  \sigma_1{:}\ldots{:}\sigma_n{:}\tup{}$.

  Let $|\bar{\sigma}|=n$ be the length of $\bar{\sigma}$ ($\tup{}$ has
  length 0).  For $1 \le i \le n$, we write $\bar{\sigma}_i$ for
  the subsequence that starts from the $i^{th}$ element of
  $\bar{\sigma}$. For $i \ge n$, we define $\bar{\sigma}_i =
  \tup{}$. In particular $\bar{\sigma} = \bar{\sigma}_1$.
  Given a permutation sequence $\sigma_1:\bar{\sigma}_2$ we define
  $head(\sigma_1:\bar{\sigma}_2)=\sigma_1$ and $head(\tup{})=\sigma_{Id}$,
  where $\sigma_{Id}$ is the identity permutation.
  We say that a permutation sequence is \emph{consistent} if all of its
  permutations are consistent.
\end{definition}

Applying a permutation sequence to a modal CNF formula can be
defined as follows:

\begin{definition}[Layered permutation of a formula]
  Let $\varphi$ be a modal CNF formula and $\bar{\sigma}$ a
  permutation sequence.  We define $\bar{\sigma}(\varphi)$
  recursively:
$$
\begin{array}{rcll}
  \tup{}(\varphi) & = & \varphi & \\
  (\sigma_1:\bar{\sigma}_2)(l) & = & \sigma_1(l) & \mbox{ for $l \in \textsf{ALit}\xspace$} \\
  (\sigma_1:\bar{\sigma}_2)(\boxr{m}C) & = & \boxr{\sigma_1(m)}\bar{\sigma}_2(C)\\
  \bar{\sigma}(C) & = & \csetsc{\bar{\sigma}(A)}{A \in C} & \mbox{ for $C$ a clause or a formula.}
\end{array}
$$
\end{definition}

Notice that layered permutations are well defined even if the modal depth
of the formula is greater than the size of the permutation sequence.
Layered permutations let us use a different permutation at each modal depth. This
enables symmetries (layered symmetries) to be found, that would not be
found otherwise.

\begin{example}
  Consider the formula $\varphi = (p \vee \boxr{m} (p \vee \neg r))
  \wedge (\neg q \vee \boxr{m} (\neg p \vee r))$. If we only consider
  non-layered symmetries then $\varphi$ has none. However,
  the permutation sequence $\tup{\sigma_1, \sigma_2}$ generated by
  $\sigma_1 = (p \ \neg q)$ and $\sigma_2 = (p \ \neg r)$ is a
  layered symmetry of $\varphi$.
\end{example}

As we can see from the previous example, layered permutations let us map
the same literal to different targets at each different modal depth.  This
additional degree of freedom can result in new symmetries for a given formula.

From now on we can mostly repeat the work we did in the previous
section to arrive to a result similar to Theorem~\ref{theo:main} but
involving permutation sequences, with one caveat: the obvious
extension of the notion of permutated model $\sigma(\mathcal{M} = \langle W,R,V \rangle)$ to layered
permutations is ill defined if $\mathcal{M} = \langle W,R,V \rangle$ is not a tree.  Hence, we need the
additional requirement that the class $\mathcal{C}\xspace$ of models is closed under
trees for the result to go through.

\begin{definition}[Layered Permutation of a model]\label{def:sigma-model}
  Let $\bar{\sigma}$ be a permutation sequence and $\mathcal{M} = \langle W,R,V \rangle = \langle w, W, V, R \rangle$
  a tree model. Then $\bar{\sigma}(\mathcal{M} = \langle W,R,V \rangle) = \langle w, W, V',R' \rangle$, where,
$$
\begin{array}{rll}

  V'(v) &=& head(\bar{\sigma}) (L_{V(v)}) \cap \textsf{Atom}\xspace \quad \mbox{for all } v \in W
  \mbox{, and, }\\
  R'(m,v)&=&\{ \bar{\sigma}_{2}(\mathcal{N}) \mid \mathcal{N} \in R(head(\bar{\sigma})(m),v)\} \quad \mbox{for all
  } m \in \textit{Mod} \mbox{ and } v \in W.
\end{array}
$$
For $M$ a set of tree models, $\bar{\sigma}(M) = \{\bar{\sigma}(\mathcal{M} = \langle W,R,V \rangle) \mid \mathcal{M} = \langle W,R,V \rangle \in M\}$.
\end{definition}

We can now extend the notion of $\sigma$-simulation to
permutation sequences.

\begin{definition}[$\bar{\sigma}$-simulation]
  Let $\bar{\sigma}$ be a permutation sequence. A
  \emph{$\bar{\sigma}$-simulation} between models
  $\mathcal{M} = \langle W,R,V \rangle=\tup{w,W,V,R}$ and $\mathcal{M} = \langle W,R,V \rangle'=\tup{w',W',V',R'}$ is a family of
  relations $Z_{\bar{\sigma}_i} \subseteq \mathrm{Ext}(\mathcal{M} = \langle W,R,V \rangle) \times \mathrm{Ext}(\mathcal{M} = \langle W,R,V \rangle')$,
  $1 \le i $, that satisfies the following conditions:

  \begin{itemize}
  \item \textbf{Root:} $\mathcal{M} = \langle W,R,V \rangle Z_{\bar{\sigma}_1} \mathcal{M} = \langle W,R,V \rangle'$.

  \item \textbf{Harmony:} If $ wZ_{\bar{\sigma}_i}w'$ then $l
    \in L_{V(w)}$ iff $head(\bar{\sigma}_i)(l) \in L_{V'(w')}$.

  \item \textbf{Zig:} If $\mathcal{M} = \langle W,R,V \rangle Z_{\bar{\sigma}_i}
    \mathcal{M} = \langle W,R,V \rangle'$ and $\mathcal{N} \in R(m,w)$ then $\mathcal{N} Z_{\bar{\sigma}_{i+1}} \mathcal{N}'$ for
    some $\mathcal{N}' \in R'(head(\bar{\sigma}_i)(m),w')$.

  \item \textbf{Zag:} If $\mathcal{M} = \langle W,R,V \rangle Z_{\bar{\sigma}_i}
    \mathcal{M} = \langle W,R,V \rangle'$ and $\mathcal{N}' \in R'(m,w')$ then $\mathcal{N} Z_{\bar{\sigma}_{i+1}} \mathcal{N}'$
    for some $\mathcal{N} \in R(head(\bar{\sigma}_i)^{-1}(m),w)$.
  \end{itemize}

  We say that two models $\mathcal{M} = \langle W,R,V \rangle$ and $\mathcal{M} = \langle W,R,V \rangle'$ are $\bar{\sigma}$-similar
  (notation $\mathcal{M} = \langle W,R,V \rangle \,\underline{\shortrightarrow}_{\bar{\sigma}}\, \mathcal{M} = \langle W,R,V \rangle')$, if there is a $\bar{\sigma}$-simulation
  between them.
\end{definition}

An important remark about the previous definition is that it does not make
any assumption about the size of the permutation sequence. In fact, it is
well defined even if the permutation sequence at hand is the empty
sequence. In that case, it just behave as the identity permutation at each
layer, thus the relation defines a bisimulation between the models.

Given a closed class of tree models $\mathcal{C}\xspace$ and $\bar{\sigma}$ a
permutation sequence, we say that $\mathcal{C}\xspace$ is \emph{closed under
  $\bar{\sigma}$} if for every $\mathcal{M} = \langle W,R,V \rangle \in \mathcal{C}\xspace$, $\bar{\sigma} (\mathcal{M} = \langle W,R,V \rangle) \in
\mathcal{C}\xspace$.

Now we are ready to prove the main result concerning layered
symmetries and entailment.

\begin{theorem}\label{theo:main2}
  Let $\varphi$ and $\psi$ be modal formulas and let $\bar{\sigma}$ be
  a consistent permutation sequence, and
  let $\mathcal{C}\xspace$ be a class of models closed under trees and $\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}$ closed under
  $\bar{\sigma}$.  If $\bar{\sigma}$ is a symmetry of $\varphi$ then
  for any $\psi$ we have that $\varphi \models_\mathcal{C}\xspace \psi$ if and only if
  $\varphi \models_\mathcal{C}\xspace \bar{\sigma}(\psi)$.
\end{theorem}

\begin{proof}
  We first show that under the hypothesis of the theorem the following
  two properties hold. \smallskip

  \noindent
  \textit{Claim 1:} $\textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi) =
  \bar{\sigma}(\textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi))$.

  \smallskip The argument is the same as for the Claim in Theorem
  \ref{theo:main} but using permutation sequences.  \medskip

\noindent
\textit{Claim 2:} $\textit{Mod}_{\mathcal{C}\xspace}(\varphi) \models_{\mathcal{C}\xspace} \varphi \mbox{
  iff } \textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi) \models_{\mathcal{C}\xspace} \varphi$.

\smallskip The left-to-right direction is trivial by the fact that
$\textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi) \subseteq \textit{Mod}_{\mathcal{C}\xspace}(\varphi)$.
For the other direction, assume $\textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi)
\models_{\mathcal{C}\xspace} \varphi$ and $\textit{Mod}_{\mathcal{C}\xspace}(\varphi) \not \models_{\mathcal{C}\xspace}
\varphi$. Then there is $\mathcal{M} = \langle W,R,V \rangle \in \textit{Mod}_{\mathcal{C}\xspace}(\varphi)$ such that $\mathcal{M} = \langle W,R,V \rangle
\not \models_{\mathcal{C}\xspace} \varphi$. But we know that $\mathcal{M} = \langle W,R,V \rangle \mathop{\underline{\leftrightarrow}} \mathcal{T}$, and
$\mathcal{T} \in \textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi)$. Hence $\mathcal{T}
\models_{\mathcal{C}\xspace} \varphi$ which contradicts our assumption.

\medskip It rests to prove that $\varphi \models_{\mathcal{C}\xspace} \psi$ if
and only if $\varphi \models_{\mathcal{C}\xspace} \bar{\sigma}(\psi)$.  By
definition, $\varphi \models_{\mathcal{C}\xspace} \psi$ if and only if
$\textit{Mod}_{\mathcal{C}\xspace}(\varphi) \models_{\mathcal{C}\xspace} \psi$. By Claim 2, this is case if
and only if $\textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi) \models_{\mathcal{C}\xspace} \psi$.
By the layered version of Proposition~\ref{prop:lit3}, this is
the case if and only if $\bar{\sigma}(\textit{Mod}_{\mathcal{C}\xspace \cap
  \mathcal{C}\xspace_{Tree}}(\varphi)) \models_{\mathcal{C}\xspace} \bar{\sigma}(\psi)$.  Given that
$\bar{\sigma}$ is a symmetry of $\varphi$, by Claim 1,
$\bar{\sigma}(\textit{Mod}_{\mathcal{C}\xspace \cap \mathcal{C}\xspace_{Tree}}(\varphi)) \models_{\mathcal{C}\xspace}
\bar{\sigma}(\psi)$ if and only if $\textit{Mod}_{\mathcal{C}\xspace \cap
  \mathcal{C}\xspace_{Tree}}(\varphi) \models_{\mathcal{C}\xspace} \bar{\sigma}(\psi)$, which by
Claim 2 is the case if and only if $\textit{Mod}_{\mathcal{C}\xspace}(\varphi) \models_{\mathcal{C}\xspace}
\bar{\sigma}(\psi)$ which by definition means that $\varphi
\models_{\mathcal{C}\xspace} \bar{\sigma}(\psi)$.
\end{proof}

\section{Modal Symmetries}\label{sec:lit-symm}

We will show that consistent symmetries for modal
 formulas behave similarly as in the propositional case and, hence,
 could assist in modal theorem proving.  Let us start by introducing
 the basic notions.

 \begin{definition}[Complete, Consistent and Generated sets of
   literals]
     A set of literals $L$ is \emph{complete} if for each $a \in \textsf{Atom}\xspace$
  either $a \in L$ or $\neg a \in L$. It is \emph{consistent} if for
  each $a \in \textsf{Atom}\xspace$ either $a \not \in L$ or $\neg a \not \in L$. Any
  complete and consistent set of literals $L$ defines a unique
  valuation $v \subseteq \textsf{Atom}\xspace$ as $a \in v$ if $a
  \in L$ and $a \not \in v$ if $\neg a \in L$.  For $S \subseteq
  \textsf{Atom}\xspace$, the \emph{consistent and complete set of literals generated
    by} $S$ (notation $L_{S}$) is $S \cup \{\neg a \mid a \in \textsf{Atom}\xspace
  \backslash S \}$.
 \end{definition}

\begin{definition}[Permutation]
  A \emph{permutation} is a bijective function $\sigma : \textsf{ALit}\xspace \mapsto
  \textsf{ALit}\xspace$. For $L$ a set of literals, $\sigma(L) = \{\sigma(l) \mid l
  \in L\}$.
\end{definition}

In this work, we only deal with permutations defined over finite sets
of literals, namely, those occurring in the formula $\varphi$ under
consideration. This restricts us to finite groups of
symmetries~\cite{fraleigh2003first}. This kind of permutations can be
succinctly defined using cyclic notation, e.g., $\sigma=(p \ \neg
q)(\neg p \ q)$ is the permutation that makes $\sigma(p)=\neg q$,
$\sigma(\neg q)= p$, $\sigma(\neg p)= q$ and $\sigma(q)= \neg p$ and
leaves unchanged all other literals; $\sigma=(p\ q\ r)(\neg p\ \neg q\
\neg r)$ is the permutation $\sigma(p)=q$, $\sigma(q)=r$ and
$\sigma(r)=p$ and similarly for the negations. Finally, for $n \in
\mathbb{Z}_{\geq 1}$ and $\sigma$ a permutation, we denote the composition of
$\sigma$ with itself $n$ times by $\sigma^n$. $\sigma^0$ denote the
identity permutation, $\sigma^{-1}$ the inverse of $\sigma$, and
$\sigma^{-n}$, for $n \in \mathbb{Z}_{\leq 1}$ is the $n$-times composition of
$\sigma^{-1}$ with itself.

Because, in our language, atoms may occur in some modalities (like $@_i$) we should take
some care when we apply permutations to modal formulas.  We will say
that a modality is \emph{indexed by atoms} if its definition depends
on the value of an atom. If $m$ is indexed by an atom $a$ we will
sometimes write $m(a)$.

\begin{definition}\label{def:permutation}[Permutation of a formula]
  Let $\varphi$ be a modal CNF formula and $\sigma$ a permutation.
  We define $\sigma(\varphi)$ recursively:
$$
\begin{array}{rcll}
  \sigma(\varphi) & = & \csetsc{\sigma(C)}{C \in \varphi} & \mbox{ for
    $\varphi$ a modal CNF formula}\\
  \sigma(C) & = & \csetsc{\sigma(A)}{A \in C} & \mbox{ for $C$ a modal
    CNF clause}\\
  \sigma(\boxr{m}C) & = & \boxr{\sigma(m)}\sigma(C) &\\
  \sigma(\neg\boxr{m}C) & = & \neg\boxr{\sigma(m)}\sigma(C) &\\
\end{array}
$$
where $\sigma(m) =\sigma(m(a)) = m(\sigma(a))$ if $m$ is indexed by $a$, and
$\sigma(m) = m$ otherwise.
\end{definition}

\begin{definition}
  A permutation $\sigma$ is \emph{consistent} if for every
  literal $l$, $\sigma (\neg l) = \neg \sigma (l)$. A
  permutation $\sigma$ is a \emph{symmetry} for $\varphi$ if $\varphi
  = \sigma(\varphi)$, when conjunctions and disjunctions in $\varphi$
  are represented as sets.
\end{definition}

\begin{example} Trivially, the identity permutation $\sigma(l) = l$ is
  a consistent symmetry of any formula $\varphi$. More interestingly,
  consider $\varphi = \{\{\neg p, r\}$, $\{q, r\}$, $\{r,[m]\{\neg p,$
  $q\}\}\}$, then the permutation $\sigma = (p\ \neg q)(\neg p\ q)$
  is a consistent symmetry of $\varphi$.
\end{example}

Now, since a permutation over literals can be lifted to transform
some formula $\varphi$ into another formula $\sigma(\varphi)$,
we also want to consider permutations applied to models.
Indeed, if $\varphi$ is true in some $\mathcal{M} = \langle W,R,V \rangle$, we intuitively want
$\sigma(\varphi)$ to be true in some model obtained from lifting
$\sigma$ to $\mathcal{M} = \langle W,R,V \rangle$.
Thus the next step is
to define the notion of applying permutations to models.

\begin{definition}[Permutation of a model]\label{def:sigma-model2}
  Let $\sigma$ be a permutation and $\mathcal{M} = \langle W,R,V \rangle = \langle w, W, V, R \rangle$
  a model. Then $\sigma(\mathcal{M} = \langle W,R,V \rangle) = \langle w, W, V',R' \rangle$, where,
$$
\begin{array}{rll}

  V'(v) &=& \sigma (L_{V(v)}) \cap \textsf{Atom}\xspace \quad \mbox{for all } v \in W
  \mbox{, and, }\\
  R'(m,v)&=&\{ \sigma(\mathcal{N}) \mid \mathcal{N} \in R(\sigma(m),v)\} \quad \mbox{for all
  } m \in \textit{Mod} \mbox{ and } v \in W.
\end{array}
$$
For $M$ a set of models, $\sigma(M) = \{\sigma(\mathcal{M} = \langle W,R,V \rangle) \mid \mathcal{M} = \langle W,R,V \rangle \in M\}$.
\end{definition}

The main ingredient to prove that symmetries preserve entailment is the
relation between models that we call $\sigma$-simulation.

\begin{definition}[$\sigma$-simulation]\label{def:sigma-sim}
  Let $\sigma$ be a permutation. A \emph{$\sigma$-simulation} between
  models $\mathcal{M} = \langle W,R,V \rangle = \langle w, W,V,R \rangle$ and $\mathcal{M} = \langle W,R,V \rangle' = \langle
  w',W',V',R' \rangle$ is a non-empty relation $Z \subseteq \mathrm{Ext}(\mathcal{M} = \langle W,R,V \rangle)
  \times \mathrm{Ext}(\mathcal{M} = \langle W,R,V \rangle')$ that satisfies the following conditions:

  \begin{itemize}
  \item \textbf{Root:} $\mathcal{M} = \langle W,R,V \rangle Z \mathcal{M} = \langle W,R,V \rangle'$.

  \item \textbf{Harmony:} $l \in L_{V(w)}$ iff $\sigma (l) \in
    L_{V'(w')}$.
  \item \textbf{Zig:} If $\mathcal{M} = \langle W,R,V \rangle Z \mathcal{M} = \langle W,R,V \rangle'$ and $\mathcal{N} \in R(m,w)$ then $\mathcal{N} Z \mathcal{N}'$ for some $\mathcal{N}'
    \in R'(\sigma(m),w')$.

  \item \textbf{Zag:} If $\mathcal{M} = \langle W,R,V \rangle Z \mathcal{M} = \langle W,R,V \rangle'$ and $\mathcal{N}' \in R'(m,w')$ then $\mathcal{N} Z \mathcal{N}'$ for some
    $\mathcal{N} \in R(\sigma^{-1}(m),w)$.
  \end{itemize}

  We say that two models $\mathcal{M} = \langle W,R,V \rangle$ and $\mathcal{M} = \langle W,R,V \rangle'$ are $\sigma$-similar (notation
  $\mathcal{M} = \langle W,R,V \rangle \,\underline{\shortrightarrow}_\sigma\, \mathcal{M} = \langle W,R,V \rangle'$) if there is a $\sigma$-simulation $Z$ between them.
\end{definition}

Notice that while $\mathcal{M} = \langle W,R,V \rangle \,\underline{\shortrightarrow}_\sigma\, \mathcal{M} = \langle W,R,V \rangle'$ implies $\mathcal{M} = \langle W,R,V \rangle' \,\underline{\shortrightarrow}_{\sigma^{-1}}\, \mathcal{M} = \langle W,R,V \rangle$, the relation
$\,\underline{\shortrightarrow}_\sigma\,$ is not symmetric (in particular $\sigma$ might differ from
$\sigma^{-1}$).
From the definition of $\sigma$-simulations it intuitively follows
that while they do not preserve validity of modal formulas (as is the
case with bisimulations) they do preserve validity of
\emph{permutations} of formulas.

\begin{proposition}\label{prop:lit2}
  Let $\sigma$ be a consistent permutation, $\varphi$ a modal CNF formula
  and $\mathcal{M} = \langle W,R,V \rangle=\tup{w,W,V,R}$, $\mathcal{M} = \langle W,R,V \rangle'=\tup{w',W',V',R'}$ models such that
  $\mathcal{M} = \langle W,R,V \rangle\,\underline{\shortrightarrow}_\sigma\, \mathcal{M} = \langle W,R,V \rangle'$.  Then $\mathcal{M} = \langle W,R,V \rangle \models \varphi$ iff $\mathcal{M} = \langle W,R,V \rangle' \models \sigma
  (\varphi)$.
\end{proposition}

\begin{proof}
  The proof is by induction on
  $\varphi$.
  Base Case: Suppose $\varphi = a$ then, $\mathcal{M} = \langle W,R,V \rangle \models a$ iff $a \in
  V(w)$ iff $a \in L_{V(w)}$ iff, by definition of
  $\sigma$-simulation, $\sigma(a) \in L_{V'(w')}$ iff $\mathcal{M} = \langle W,R,V \rangle' \models
  \sigma(a)$.

  Suppose $\varphi = \neg a$ then, $\mathcal{M} = \langle W,R,V \rangle \models \neg a$ iff $a \not\in
  V(w)$ iff $\neg a \in L_{V(w)}$ iff, by definition of
  $\sigma$-simulation, $\sigma(\neg a) = \neg \sigma(a) \in
  L_{V'(w')}$ iff $\sigma(a) \not\in V'(w')$ iff $\mathcal{M} = \langle W,R,V \rangle' \models \neg
  \sigma(a)$.

  When $\varphi=C$, with $C$ a clause or a conjunction of
  clauses, the proof follows by induction directly.

  Inductive Step: Suppose $\varphi = \boxr{m} \psi$. Then $\mathcal{M} = \langle W,R,V \rangle \models
  \boxr{m} \psi$ iff $\mathcal{N} \models \psi$ for all $\mathcal{N} \in R(m,w)$. Given
  that $\mathcal{M} = \langle W,R,V \rangle\,\underline{\shortrightarrow}_\sigma\, \mathcal{M} = \langle W,R,V \rangle'$, by Zig we know that for all $\mathcal{N}$ exist $\mathcal{N}'$
  such that $\mathcal{N} \,\underline{\shortrightarrow}_\sigma\, \mathcal{N}'$ and $\mathcal{N}' \in R'(\sigma(m),w')$. Then, by
  inductive hypothesis, $\mathcal{N}' \models \sigma(\psi)$ for all $\mathcal{N}' \in
  R'(\sigma(m),w')$ iff $\mathcal{M} = \langle W,R,V \rangle' \models \boxr{\sigma(m)}\sigma(\psi)$.
  Then, by Definition \ref{def:permutation}, $\mathcal{M} = \langle W,R,V \rangle' \models
  \sigma(\boxr{m}\psi)$.  The converse uses Zag and the inductive hypothesis.

  Suppose $\varphi = \neg \boxr{m} \psi$. Then $\mathcal{M} = \langle W,R,V \rangle \models
  \neg \boxr{m} \psi$ iff there exists $\mathcal{N} \in R(m,w)$ such that, $\mathcal{N} \models
  \neg \psi$. Given
  that $\mathcal{M} = \langle W,R,V \rangle\,\underline{\shortrightarrow}_\sigma\, \mathcal{M} = \langle W,R,V \rangle'$, by Zig we know that for all $\mathcal{N}$ exist $\mathcal{N}'$
  such that $\mathcal{N} \,\underline{\shortrightarrow}_\sigma\, \mathcal{N}'$ and $\mathcal{N}' \in R'(\sigma(m),w')$. Then, by
  inductive hypothesis, $\mathcal{N}' \models \sigma(\neg \psi) = \neg
  \sigma(\psi)$ iff $\mathcal{M} = \langle W,R,V \rangle' \models \neg \boxr{\sigma(m)}\sigma(\psi)$.
  Then, by Definition \ref{def:permutation}, $\mathcal{M} = \langle W,R,V \rangle' \models
  \sigma(\neg \boxr{m}\psi)$.  The converse follows using Zag and the inductive hypothesis.
\end{proof}

An easily verifiable consequence of Definitions~\ref{def:sigma-model2}
and~\ref{def:sigma-sim} is that $\mathcal{M} = \langle W,R,V \rangle$ and $\sigma(\mathcal{M} = \langle W,R,V \rangle)$ are always
$\sigma$-similar.

\begin{proposition} \label{prop:lit1} Let $\sigma$ be a consistent
  permutation and $\mathcal{M} = \langle w,W,V,R \rangle$ a
  model. Then $\mathcal{M} \,\underline{\shortrightarrow}_\sigma\, \sigma (\mathcal{M})$.
\end{proposition}

\begin{proof}
  Let us define the relation $Z=\{ (\mathcal{N},\sigma(\mathcal{N})) \mid \mathcal{N} \in
  \mathrm{Ext}(\mathcal{M} = \langle W,R,V \rangle) \}$ and show that it is a $\sigma$-simulation between $\mathcal{M} = \langle W,R,V \rangle$
  and $\sigma(\mathcal{M} = \langle W,R,V \rangle)$.  The \textit{Zig} and \textit{Zag} conditions are
  trivial by definition of $\sigma(\mathcal{M} = \langle W,R,V \rangle)$.

  For \textit{Harmony}, we have to check that $l \in L_{V(w)}$
  iff $\sigma (l) \in L_{V'(w)}$. From the definition of $\sigma
  (\mathcal{M} = \langle W,R,V \rangle)$, $L_{V'(w)} = \sigma (L_{V(w)})$, hence if $l \in L_{V(w)}$
  then $\sigma(l) \in \sigma(L_{V(w)})$.  Moreover, $\sigma
  (L_{V(w)})$ is a complete set of literals because $L_{V(w)}$ is a
  complete set of literals and $\sigma$ is a consistent permutation,
  and hence the converse also follows.
\end{proof}

Interestingly, if $\sigma$ is a symmetry of $\varphi$ then for any
model $\mathcal{M} = \langle W,R,V \rangle$, $\mathcal{M} = \langle W,R,V \rangle$ is a model of $\varphi$ if and only if $\sigma(\mathcal{M} = \langle W,R,V \rangle)$
is. This will be a direct corollary of the following proposition in
the particular case when $\sigma$ is a symmetry and hence
$\sigma(\varphi) = \varphi$.

\begin{proposition}\label{prop:lit3}
  Let $\sigma$ be a consistent permutation, $\mathcal{M} = \langle W,R,V \rangle$ a model and $\varphi$
  a modal CNF formula. Then $\mathcal{M} = \langle W,R,V \rangle \models \varphi$ iff $\sigma (\mathcal{M} = \langle W,R,V \rangle)
  \models \sigma (\varphi)$.
\end{proposition}

 \begin{proof}
   From Proposition~\ref{prop:lit1} ($\mathcal{M} = \langle W,R,V \rangle
   \,\underline{\shortrightarrow}_\sigma\, \sigma(\mathcal{M} = \langle W,R,V \rangle)$) and Proposition~\ref{prop:lit2}.
 \end{proof}

\begin{corollary}\label{cor:lit4}
  If $\sigma$ is a symmetry of $\varphi$ then $\mathcal{M} = \langle W,R,V \rangle \in \textit{Mod}(\varphi)$
  iff $\sigma(\mathcal{M} = \langle W,R,V \rangle) \in \textit{Mod}(\varphi)$.
\end{corollary}

To clarify the implications of the Corollary~\ref{cor:lit4}, consider
the following example.

\begin{example}
  Let $\varphi = (p \vee q \vee r) \wedge (s \vee q \vee r) \wedge
  (\neg p \vee \neg s) \wedge \tup{m} ( p \vee s ) \wedge [\mathsf{A}]( \neg r
  ) $.
  From Figure~\ref{fig:coroll}a we can verify
  that $\mathcal{M} = \langle W,R,V \rangle_{1} \models \varphi$.

  Now $\sigma = (p\ s)(\neg p\ \neg s)$ is a symmetry of $\varphi$.
  Then, by Corollary~\ref{cor:lit4}, we have
  $\sigma(\mathcal{M} = \langle W,R,V \rangle_{1}) \models \varphi$, which can be verified in the
  model of Figure~\ref{fig:coroll}b.

\begin{figure}[ht]
  \begin{center}
    \begin{minipage}[ht]{.45\linewidth}
      \begin{center}
        \includegraphics[scale=0.6,keepaspectratio=true]{images/corollary}

        (a)
      \end{center}
    \end{minipage}

    \begin{minipage}[ht]{.45\linewidth}
      \begin{center}
        \includegraphics[scale=0.6,keepaspectratio=true]{images/corollary-2}

        (b)
      \end{center}
    \end{minipage}
  \end{center}
  \caption{a) Model $\mathcal{M} = \langle W,R,V \rangle_{1}$. b) Model $\sigma(\mathcal{M} = \langle W,R,V \rangle_{1})$.  \label{fig:coroll}}
\end{figure}

\end{example}

The notion of $\sigma$-simulation in coinductive modal models is
general enough to be applicable to a wide range of modal logics.
Notice though, that our definition of $\sigma$-simulation makes no
assumption about the models being in the same class. Consider, for
example, a model $\mathcal{M} = \langle W,R,V \rangle \in \mathcal{C}\xspace_{\mathcal{H}\xspace(@)}$ and a permutation $\sigma = (i\
p)(\neg i \ \neg p)$ for $i \in \textsf{Nom}\xspace$, $p \in \textsf{Prop}\xspace$. By the defining
condition $\mathcal{C}\xspace_{\mathcal{H}\xspace(@)}$, nominals in $\mathcal{M} = \langle W,R,V \rangle$ are true at a unique
element in the domain, but this does not necessary hold for
$\sigma(\mathcal{M} = \langle W,R,V \rangle)$, and hence $\sigma(\mathcal{M} = \langle W,R,V \rangle)$ might not be in
$\mathcal{C}\xspace_{\mathcal{H}\xspace(@)}$. Hence, when working with subclasses of $\mathbf{Mods}$ we will
often have to require additional conditions to a permutation $\sigma$
to ensure that for every $\mathcal{M} = \langle W,R,V \rangle$, $\sigma(\mathcal{M} = \langle W,R,V \rangle)$ is in the intended class.

\begin{definition}
  Let $\sigma$ be a permutation and $\mathcal{C}\xspace$ a closed class of models. We
  say that $\mathcal{C}\xspace$ is \emph{closed under $\sigma$} if for every $\mathcal{M} = \langle W,R,V \rangle \in
  \mathcal{C}\xspace$, $\sigma(\mathcal{M} = \langle W,R,V \rangle) \in \mathcal{C}\xspace$.
\end{definition}

\begin{example}[$\sigma$-simulation in hybrid logic]
  Consider the class $\mathcal{C}\xspace_{\mathcal{H}\xspace(@)}$. $\mathcal{C}\xspace_{\mathcal{H}\xspace(@)}$ is not closed under arbitrary permutations, but it is
  closed under permutations that send nominals to nominals.

\end{example}

Everything is now in place to show that modal entailment is preserved
under symmetries.

 \begin{theorem}\label{theo:main}
   Let $\varphi$ and $\psi$ be modal formulas, let $\sigma$ be a
   consistent symmetry of $\varphi$ and $\mathcal{C}\xspace$ a class of models closed
   under $\sigma$. Then $\varphi \models_{\mathcal{C}\xspace} \psi$ if and only if
   $\varphi \models_{\mathcal{C}\xspace} \sigma(\psi)$.
 \end{theorem}

\begin{proof}
  We first show that under the hypothesis of the theorem the following
  property holds \smallskip

  \noindent
  \textbf{Claim:} $\textit{Mod}_{\mathcal{C}\xspace}(\varphi) = \sigma(\textit{Mod}_{\mathcal{C}\xspace}(\varphi))$.
  \smallskip

  \noindent [$\supseteq$] Let $\mathcal{N} \in
  \sigma(\textit{Mod}_{\mathcal{C}\xspace}(\varphi))$ and $\mathcal{M} = \langle W,R,V \rangle \in \textit{Mod}_{\mathcal{C}\xspace}(\varphi)$ be
  such that $\mathcal{N} = \sigma (\mathcal{M} = \langle W,R,V \rangle)$.  Then $\mathcal{M} = \langle W,R,V \rangle \models \varphi$
  and by Corollary~\ref{cor:lit4}, $\sigma (\mathcal{M} = \langle W,R,V \rangle) \models \varphi$. Given
  that $\mathcal{C}\xspace$ is closed under $\sigma$, $\sigma (\mathcal{M} = \langle W,R,V \rangle) \in \mathcal{C}\xspace$ and,
  hence, $\sigma (\mathcal{M} = \langle W,R,V \rangle) \in \textit{Mod}_{\mathcal{C}\xspace}(\varphi)$.  \smallskip

  \noindent [$\subseteq$] Let $\mathcal{M} = \langle W,R,V \rangle \in \textit{Mod}_{\mathcal{C}\xspace}(\varphi)$, then $\mathcal{M} = \langle W,R,V \rangle
  \models \varphi$.   By Corollary~\ref{cor:lit4}, $\sigma (\mathcal{M} = \langle W,R,V \rangle) \models
  \varphi$ and, given that $\mathcal{C}\xspace$ is closed under $\sigma$, $\sigma
  (\mathcal{M} = \langle W,R,V \rangle) \in \mathcal{C}\xspace$. Therefore, $\sigma (\mathcal{M} = \langle W,R,V \rangle) \in
  \textit{Mod}_{\mathcal{C}\xspace}(\varphi)$.  Because $\sigma$ is arbitrary, the results holds
  also for $\sigma^k$, $k \in \mathbb{Z}$.

  Because $\sigma$ is a permutation over a finite set, there exists $n$
  such that $\sigma^n$ is the identity permutation.
  Now consider $\sigma^{n-1}(\mathcal{M} = \langle W,R,V \rangle)$, we know $\sigma^{n-1}(\mathcal{M} = \langle W,R,V \rangle) \in
  \textit{Mod}_{\mathcal{C}\xspace}(\varphi)$. Hence $\sigma^n(\mathcal{M} = \langle W,R,V \rangle) = \mathcal{M} = \langle W,R,V \rangle \in
  \sigma(\textit{Mod}_{\mathcal{C}\xspace}(\varphi))$.\medskip

  Now, we have to prove that $\varphi \models_{\mathcal{C}\xspace} \psi$ iff
  $\varphi \models_{\mathcal{C}\xspace} \sigma(\psi)$.  By definition, $\varphi \models_{\mathcal{C}\xspace}
  \psi$ iff $\textit{Mod}_{\mathcal{C}\xspace}(\varphi) \models_{\mathcal{C}\xspace} \psi$. By
  Proposition~\ref{prop:lit3}, this is the case if and only if
  $\sigma(\textit{Mod}_{\mathcal{C}\xspace}(\varphi)) \models_{\mathcal{C}\xspace} \sigma(\psi)$.

  Given that $\sigma$ is a symmetry of $\varphi$, by the Claim above,
  $\sigma(\textit{Mod}_{\mathcal{C}\xspace}(\varphi)) \models_{\mathcal{C}\xspace} \sigma(\psi)$ iff
  $\textit{Mod}_{\mathcal{C}\xspace}(\varphi) \models_{\mathcal{C}\xspace} \sigma(\psi)$, which by definition
  means $\varphi \models_{\mathcal{C}\xspace} \sigma(\psi)$.
\end{proof}

Theorem~\ref{theo:main} provides an inexpensive inference mechanism
that can be used in every situation where entailment is involved
during modal automated reasoning.
Indeed, applying a permutation on a formula is a calculation that is
arguably computationally cheaper than a tableau expansion or a resolution
step. Therefore, new formulas obtained by this mean may reduce
the total running time of an inference algorithm.
In the case of propositional logic, the strengthening of the learning
mechanism has already shown its results in~\cite{Benhamou:uv}.
In the case of modal logic, it remains to see when cases of $\varphi \models \psi$
occur during a decision procedure, and how to better take advantage of them.

redpajama_set_name: RedPajamaArXiv


text:
Nan Griswold
"… I learned to know the homeless and they are people just like you and me but homeless."
Nan Griswold's involvement with homelessness began in 1982 when an influx of individuals could not access emergency shelters in Winston-Salem, NC because they were full. At the time, the only shelters in town were the Winston-Salem Rescue Mission, The Salvation Army and Lighthouse. The Reverend Ginny Britt at Crisis Control Ministry, asked Nan to help find a solution to the problem. At the time, Nan served as the assistant director at Downton Church Center. She, Ginny and other concerned community members rallied together to find a solution. They came up with the idea to ask downtown churches to open their doors to individuals experiencing homelessness. She and Ginny proposed the idea to several congregations in the community, many of which agreed to participate. For approximately five years willing congregations opened their doors to people experiencing homelessness during the winter months of January through March.
In 1986 Nan and a few others were selected to be on a task force created by Mayor Wayne Corpening and Chairman of County Commissioners, Richard Linville. The task force presented six housing and basic needs recommendations to the City and County. One of the recommendations was to establish a permanent council for homeless services to improve coordination and planning of homeless services. Thus, the Homeless Council was created as a place for people and organizations with an interest in homelessness "to communicate and share ideas." The Homeless Council continues to meet every third Tuesday of the month. Nan has seen the community make great strides to strengthen the relationship amongst service providers resulting in better service to those experiencing homelessness. Nan said "we learned to work with each other; we've learned to depend on each other." Since the mid 80's, Nan has intimately been involved in the development of homeless services in Forsyth County. She is happy to see that the Homeless Council, now known as the WSFC CoC continues to support the work to end homelessness in Winston-Salem.
After her retirement as Founding Executive Director at the Second Harvest Food Bank, Nan continued to serve on the Homeless Council executive committee. The past several years she has not been as active but still concerned. However, she is still active in the community. She believes in the ministry of helping others and is committed to a life of service to others. She now serves on the Faith and Justice Committee at her church, St Paul's Episcopal Church.
Nan served on the board of Samaritan Ministries for six years and the Capital Campaign for the new building. She has been a big supporter of Samaritan Ministries since the beginning and takes immense pride in her involvement with the organization and what is has accomplished over the years. With an extensive background in social work she is familiar with interacting with youth of various backgrounds. She has worked with troubled youth in the criminal justice system and is interested in working to find housing for youth as they leave foster care.
When she is not busy addressing homelessness, she enjoys a good read and spending time with her family. As a devoted animal lover, she is also involved with the Forsyth Humane Society, where she participated on their capital campaign for their new building located on Country Club Road. Nan's passion for social justice issues continues to fuel her drive to stay active in the community. Overall, she feels fortunate to be amongst passionate colleagues and is appreciative of her longtime career.

redpajama_set_name: RedPajamaCommonCrawl


This seems to be a birthday season for Nigerian entertainers. The celebrities have taken to their social media handles to celebrate their new age and God's grace over her life.
Beautiful Nollywood actress Doris Simeon on Sunday, July 22, added a year older was highly celebrated by family, colleagues and majority of her fans on social media.
Simeon celebrated her new age by sharing stunning new pictures on Instagram. She was obviously not in Nigeria for her birthday judging from the background of the pictures she shared on social media.
The beautiful actress also shared another video of her thanking everyone who celebrated her. She also shared another video of her going shopping with her son on her birthday. Simeon really had fun with her little man.
It was earlier reported that Big Brother Naija (BBN) reality star, Vandora Williams, on Tuesday July 24, turned a year older and has taken to social media top celebrate her new age. The young lady was celebrated by former reality star housemates.


text:
package com.ryft.spark.connector.sql

import java.net.URL

import com.ryft.spark.connector.domain._
import com.ryft.spark.connector.exception.RyftSparkException
import com.ryft.spark.connector.partitioner.impl.NoPartitioner
import org.apache.spark.Logging
import org.apache.spark.sql.{DataFrame, SaveMode, SQLContext}
import org.apache.spark.sql.sources.{CreatableRelationProvider, SchemaRelationProvider, BaseRelation, RelationProvider}
import org.apache.spark.sql.types.StructType

class DefaultSource extends SchemaRelationProvider with CreatableRelationProvider with Logging {
  override def createRelation(@transient sqlContext: SQLContext,
      parameters: Map[String, String],
      schema: StructType): BaseRelation = {

    val files = parameters.getOrElse("files", {
      val msg = "Required parameter files was not specified"
      logWarning(msg)
      throw RyftSparkException(msg)
    }).split(',').toList

    val options = parameters map {case (k, v) => s"$k: $v"}

    logInfo(s"Creating Ryft Relation: " +
      s"\n${options.mkString("\n")}" +
      s"\nschema: ${schema.treeString}")
        new RyftRelation(files, schema, parameters)(sqlContext)
  }

  override def createRelation(@transient sqlContext: SQLContext,
      mode: SaveMode, // toDo: match different modes
      parameters: Map[String, String],
      data: DataFrame): BaseRelation = {

    val path = parameters.getOrElse("path", {
      val msg = "Save requires path parameter"
      logError(msg)
      throw RyftSparkException(msg)
    })

    import com.ryft.spark.connector._
    data.saveToRyft(path, parameters)

    createRelation(sqlContext, Map("files" -> path), data.schema)
  }
}

redpajama_set_name: RedPajamaGithub


text:
using Atomiv.Infrastructure.EntityFrameworkCore;
using Atomiv.Template.Core.Common.Orders;
using System;
using System.Collections.Generic;

namespace Atomiv.Template.Infrastructure.Domain.Persistence.Records
{
    public class OrderRecord : Record<Guid>
    {
        public Guid CustomerId { get; set; }

        public DateTime OrderDate { get; set; }

        public OrderStatus OrderStatusId { get; set; }

        public virtual CustomerRecord Customer { get; set; }

        public virtual OrderStatusRecord OrderStatus { get; set; }

        public virtual ICollection<OrderItemRecord> OrderItems { get; set; }
    }
}


text:
Martin E. Whelan
Martin E. Whelan, Jr. of Newport Beach died on September 11, 2015 at the age of 86.
Marty was born in Los Angeles in 1928 to Martin and Celeste Whelan and was the younger brother of Patricia Welch (deceased). He graduated from Loyola High School in 1945, Santa Clara College in 1949, and Loyola Law School in 1951, and passed the California Bar Exam at age 22. After serving in the US Army's Judge Advocate General Corps, he practiced law in Los Angeles and, from 1959 to 1982, in Whittier. He was president of the Whittier Bar Association, was elected to the first board of Whittier Junior College (Rio Hondo College) and was an active member of the East Whittier Rotary Club. He had a business law practice where he earned the reputation of being a brilliant attorney. For three decades, he was general counsel of the Water Replenishment District of Southern California and represented numerous water districts. In his retirement years in Newport Beach, he served as a Eucharistic minister at Our Lady Queen of Angels Catholic Church and enjoyed many bridge games at Big Canyon Country Club, where he was a member.
Marty is survived by Nancy (Mispagel), his beloved wife of 59 years; their five children, Daniel (Sharon), Catherine Ramsay (Sheldon), M. Edward III (Deborah), Matthew (Susan), and Monica Scarborough (Claude). He had ten grandchildren whom he adored, Christopher, Jessica, Nicholas, Jeffrey, Ian, Jack, Anne, Mary, Elizabeth Whelan and Kathryn Scarborough. He became an avid fan of USC football on his wedding day and remained so to the end.
The Mass of Christian Burial will be at Our Lady Queen of Angels Catholic Church, Newport Beach, on Saturday, September 26, 2015 at 11:00 A.M. Donations may be sent to Boy Scouts of America, Orange County Council (www.ocbsa.org) or to your favorite charity.
1 responses to Martin E. Whelan
Dan Glasgow says:
Lit a candle in memory of Martin E. Whelan


The September 9th National Prison Strike is coming up! To learn more, check out the Support Prisoner Resistance site, in particular the zines Let the Crops Rot in the Fields by the Free Alabama Movement, End Prison Slavery with several articles about emerging prisoner movements, and Incarcerated Workers Take the Lead by Houston IWOC.
In our interview with Azzurra from the Incarcerated Workers Organizing Committee, she referred to several texts, campaigns, and other resources, including: the Houston IWOC zine about the history of prisoner rebellion since 2008, the Attica Rebellion, Black August, the Flikshop app for sending postcards to prisoners easily and cheaply, Chicano anarchist political prisoner Xinachtli Alvaro Luna Hernandez and his Twitter account, Mumia Abu Jamal's struggle for Hepatits C treatment, Rashid Johnson's article "On the Questions of Race and Racism: Revolutionary National Liberation and Building the United Front Against Imperialism", checking the IWOC website for ongoing updates, Jeremy's Hammond's recent trip to solitary confinement for "encouraging rebellion and criminal activities," and criminologist Nils Christie's article Conflicts as Property about how the state has appropriated our conflicts.
On the Chopping Block, we reviewed Dan Berger's book Captive Nation: Black Prison Organizing in the Civil Rights Era. It discusses, among many other things, the life, death, and legacy of George Jackson, whose books Soledad Brother and Blood in My Eye can be read in full online.
We interviewed Jon Active from Active Distribution in the UK about the Brexit vote. If you want to read more anarchist perspectives on it, check out these articles: "Building an anti-fascist culture post-Brexit" by some folks from the Anti-Raids Network, "On the tragic and the farcical of the British referendum" by the Void Network, and anarchist reflections on Brexit on Reddit.
Please support Kara Wild, a trans anarchist from the US imprisoned in France in connection with recent militant protests in Paris. Here's a video of her in her former dwelling that she built and squatted in in Chicago. We'll post more updates on how to direct support her way as soon as we get them.
We also referenced some other queer and/or trans prisoner solidarity links, including Black and Pink, the Trans Prisoner Day of Action and Solidarity, and a publication focusing on the writings of incarcerated women and trans and gender variant prisoners called Unstoppable.
And if you're feeling down, just remember that in Phenix City, Alabama, an unnamed Taco Bell employee refused to serve four cops who came in to order food - because they were cops. That's what we mean by Fight where you stand!


Her life began like the most beautiful fairy tale, which has quickly become a nightmare.The people loved her shy smile behind which she hid all her problems.
Born Diana Spencer on July 1, 1961, Princess Diana became Lady Diana Spencer after her father inherited the title of Earl Spencer in 1975. She married heir to the Prince Charles on July 29, 1981.
Before she became a princess, Diana was a simple young girl. She never wore make-up or set foot on a plane – not until she met her prince, which she said fateful "yes" when she was only 20 years old. Diana Spencer began life in the most famous monarchy after only 6 meetings with Prince Charles.
She was young, beautiful, and a little shy young girl and it was easy to fall in love with her and what her life was in the eyes of ordinary people. Then her world has changed drastically, although she remained the old, common Diane.
Because of her uniqueness she destroyed all the myths about princesses.
Diana was the princess who has always been closer to ordinary people, but the world in which she sailed. In England, clearly, that was unacceptable.
Diana was 36 years and for the short time that was rejected by the royal family reached the popularity that is hard to measure.
She was known for her philanthropy, kindness and the scandal that surrounded her marriage, Diana, Princess of Wales, was also known for her unerring sense of style that influenced a generation of women.
Life Story, Forever Beloved Princess - Diana, Princess of Wales!


IMAGE WHEELS INTERNATIONAL LIMITED ("We") are committed to protecting and respecting your privacy.
For the purpose of the Data Protection Act 1998 (the Act), the data controller is Image Wheels International Limited of Unit 3, Fountain Lane Industrial Estate, Fountain Lane, Tipton, West Midlands, DY4 9HA.
Information that you provide by filling in forms on our site www.imagewheels.co.uk (our site). This includes information provided at the time of making an enquiry or placing an order, posting material or requesting further information.
We will only pass your details to third party carriers who deliver goods to you arising from any contracts entered into between you and us. We will never pass your details to third parties for marketing purposes unless we first obtain your consent to do so.
If Image Wheels International Limited or substantially all of its assets are acquired by a third party, in which case personal data held by it about its customers will be one of the transferred assets.
If we are under a duty to disclose or share your personal data in order to comply with any legal obligation, or in order to enforce or apply our Terms and Conditions of Supply and other agreements; or to protect the rights, property, or safety of Image Wheels International Limited, our customers, or others. This includes exchanging information with other companies and organisations for the purposes of fraud protection and credit risk reduction.
We will not process your personal data for marketing purposes unless we have your consent to do so. We will inform you if we intend to use your data for such purposes. You have the right to refuse permission for use of your data for such purposes. You can exercise this right by contacting us at Image Wheels International Limited, Unit 3, Fountain Lane Industrial Estate, Fountain Lane, Tipton, West Midlands, DY4 9HA or use our Contact Form.


Last year I posted about being a travel snob and admitted to a few violations myself. A year later I have to admit that I might be a travel snob, especially after reading this post over at View From The Wing. Below is the video, and it makes the point better than the article, sorry Gary.
Recently I was traveling with someone that had no, and I mean no status. When we approached security I went to the TSA pre-check lane, and they went to their noticeably longer lane. They didn't realize that if you have TSA pre-check (me) you can't suddenly decide to go through the Non-TSA pre-check lane (them). Insensitively I explained it this way, "No one with TSA Pre, yes we call it that, goes through the long line". On this day I was wearing my asshat shoes. It seems that when I put these on I inadvertently piss everyone off when I speak.
This exchange made me think about the new term "Mansplain". If you're not familiar with the term, see below.
In case you didn't know condescending is when you talk down to someone. See what I did there.
I propose a new term, "Travelsplain". Travelsplain, when a traveler explains travel to a non-traveler in a manner regarded as condescending or patronizing.
Scenario – Passengers, especially non-travelers, crowding the boarding area waiting for their zone to be called.
Scenario – A non-traveler breaking out a smartphone to call in order to book, change or cancel a hotel, rental car or flight reservation.
Scenario – A non-traveler arrives at the gate with more carry-on bags than the Duggar's have children.
Scenario – A non-traveler is seen boarding a SuperShuttle. The SuperShuttle provides rides to and from the airport.
All joking aside, roadwarriors try to help, but often we lack the tact needed to effectively communicate our suggestions.


I and my pals were found to be examining the great helpful hints from your website while unexpectedly developed a terrible suspicion I had not thanked the blog owner for those techniques. All the men appeared to be for that reason very interested to see them and have in effect pretty much been loving these things. Many thanks for being considerably kind and also for deciding on this kind of smart useful guides millions of individuals are really eager to discover. My personal honest regret for not saying thanks to sooner.


The annual Infecting the City Public Arts Festival is underway, transforming the streets of Cape Town into an art-filled wonderland, brimming with innovative and extraordinary exhibitions and performances.
Challenging both the conventions of traditional art and the notions of public space, Infecting the City brings disruptive and engaging art forms closer to members of the public, celebrating South Africa's rich heritage and multitude of cultures through various forms of artistic expression.
Running from the 10th - 15th of March, head down to Cape Town's city centre for a collection of free performances during both day and night time.
Click here for the full Infecting the City Public Arts Festival programme and map.
What is Grade School (GS)?
New Balance x Shelflife x Dr.Z - "City of Gold 574"


text:
Scott's Funeral Home of Copperas Cove
Send Flowers for CSM Marion
CSM Marion Lee "Butch" Mixon, US Army, Ret.
April 11, 1943 ~ January 12, 2020 (age 76)
Marion Lee "Butch" Mixon, age 76, passed away on Sunday, January 12, 2020, at home in Copperas Cove. Funeral Services will be held at 11:00 AM, Saturday, January 18, 2020, at Clear Creek Baptist Church, 3350 FM 2657 in Kempner. Visitation will be an hour prior to the service at the church.
Butch was the eldest of nine children born to the late Vester Morgan Mixon SR. and Myrtle Lucille Brinkley Mixon on April 11, 1943. He and Patsy Jean Brewer married September 1, 1967, in Wichita Falls, Texas. While in the military over 27 years, The US Air Force 1960-1964 SAC Grand Forks ND./ US Army 1965-1987, he saw assignments in the United States, Germany, Korea and two tours in Vietnam 1st Cav 65-66, 101st 68-69, attaining the rank of Command Sergeant Major and numerous military awards. His assignments included special mission assignments most of his Army Career which included assignment to all 3 Airmobile Divisions 11th Air Assault/1st Cav Airmobile Division/ 101st Airborne, CH-47 Training units at Ft Sill (154th Avn.) and Ft Benning (177th/205th Avn.). Ft. Benning also included flying duties as a Flight Engineer on one of 2 CH-47 Helicopters supporting The United States Army Executive Flight Detachment (Army One) for the Nixon Administration, Nuke Security units in Germany (205th Avn.) and Ft. Carson ()179th Avn.), with later assignment to The United States Army Executive Flight Detachment (Army One) supporting the Ford Administration until unit was deactivated with total mission given to Marine One in 1976, 1st US Army Advisor to United States Army Reserves units assigned to the FT. Meade Flight Facility, 1st Sgt of half American half R.O.K. Army unit in Korea (117th Avn), 1 Sgt. C Company 34th Support 6th Cav Brigade), USASMA Fort Bliss, 1st Sgt B Troop and HHT 2/1 Cav Fort Lewis WA., CSM 502nd Avn BN. Fort Hood, with final assignment as the CSM of 2AD Aviation Brigade, Ft. Hood.
Upon retirement from the military he was employed by DynCorp from 1988-2004 working as an Aircraft Mechanic, Aircraft Inspector, Aircraft Lead, Production Control Manager and Quality Control Manager. Duties with DynCorp allowed him to continue his love of flying as a Flight Engineer on his beloved 47's and crew chief on UH-1's in several states and Egypt.
Butch is preceded in death by his parents; sisters, Cynthia Ann Mixon Beam, Rosland Gail Mixon; brothers, Vester Morgan Mixon Jr., Rusty Ray Mixon; sister-in-laws, June Brewer, Karen Brewer O'Malley; brother-in-laws, Virgil Lee Brewer, Marlin Ranze Allison SR., and Jerry Goeringer.
Butch is survived by his wife, Patsy Jean Brewer Mixon; son, Jesse Morgan Mixon; daughters Melody Lynn Rowe and husband, Kevin, Marian Lea Mixon Johnson and husband, Glenn; grandchildren, Genny Rayfield, Tony Lugo and wife, Amanda Trubee, Amy Johnson Blackburn, Morgan Mixon Surratt and husband, Toby, Mandy Mixon and Brady Rowe; brother, Arvil Ray Mixon I; sisters, Beverly Joyce Mixon Hill, Sandra Kay Mixon Scott and husband, Earl, Melinda Francinn Mixon Ketchum; and brother-in-law's, Donald Leroy Beam, Jesse Van Brewer and wife, Kay; sister-in-law's, Mary Laddie Brewer Goeringer, Ada Darlene Green Brewer, Jackie Jensen Mixon and numerous nephews and nieces.
In lieu of flowers, memorials may be made to Home for our Troops at 866-787-6677 or at hfotusa.org.
To send flowers to CSM Marion Lee "Butch" Mixon, US Army, Ret.'s family, please visit our floral section.
Clear Creek Baptist Church
Kempner, Texas 76539
© 2020 Scott's Funeral Home of Copperas Cove. All Rights Reserved. Funeral Home website by CFS