1a38107941725211e7c3f051f7a8f5e12199f03acmaeder\documentclass{entcs} \usepackage{entcsmacro}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\usepackage{graphicx}

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner\usepackage{mathpartir}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\sloppy

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% The following is enclosed to allow easy detection of differences in

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu% ascii coding.

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Upper-case A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder% Lower-case a b c d e f g h i j k l m n o p q r s t u v w x y z

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Digits 0 1 2 3 4 5 6 7 8 9

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Exclamation ! Double quote " Hash (number) #

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Dollar $ Percent % Ampersand &

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Acute accent ' Left paren ( Right paren )

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Asterisk * Plus + Comma ,

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Minus - Point . Solidus /

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Colon : Semicolon ; Less than <

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Equals =3D Greater than > Question mark ?

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% At @ Left bracket [ Backslash \

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Right bracket ] Circumflex ^ Underscore _

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Grave accent ` Left brace { Vertical bar |

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder% Right brace } Tilde ~

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder% A couple of exemplary definitions:

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\newcommand{\Nat}{{\mathbb N}}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\newcommand{\Real}{{\mathbb R}}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\def\lastname{Hausmann and Schr\"oder}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\begin{document}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{frontmatter}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \title{Optimizing Conditional Logic (Draft)}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \author[Bremen]{Daniel Hausmann\thanksref{ALL}\thanksref{myemail}}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \author[Bremen]{Lutz Schr\"oder\thanksref{ALL}\thanksref{coemail}}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \address[Bremen]{Deutsches Zentrum f\"ur k\"unstliche Intelligenz (DFKI)\\ Universit\"at Bremen, Germany}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \thanks[ALL]{This work is supported by DFG-project no1234}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \thanks[myemail]{Email: \href{mailto:Daniel.Hausmann@dfki.de} {\texttt{\normalshape Daniel.Hausmann@dfki.de}}}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \thanks[coemail]{Email: \href{mailto:Lutz.Schroeder@dfki.de} {\texttt{\normalshape Lutz.Schroeder@dfki.de}}}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{abstract}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder We describe a specific optimization of the decision algorithm

1a38107941725211e7c3f051f7a8f5e12199f03acmaederof conditional logic. The general framework

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder of this optimization is the setting of coalgebraic modal logic,

1a38107941725211e7c3f051f7a8f5e12199f03acmaederthe actual implementation is an extension to

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder the generic satisfiability solver for modal logics CoLoSS.

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{abstract}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{keyword}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Coalgebraic modal logic, conditional logic,

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedersatisfiability / provability, optimization by memoizing

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\end{keyword}

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder\end{frontmatter}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\section{Introduction}\label{intro}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaederIntroduce here :)

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederStructure of the paper: First we give a short introduction to

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederthe theory of coalgebraic modal logics, the general abstract

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroedersetting in which this paper takes place. Then we describe the

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedersatisfiability (and provability) solving algorithm and its

1a38107941725211e7c3f051f7a8f5e12199f03acmaederoptimization with regards to conditional logics. Further, we

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederanalyze the quality of this optimization by relating

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederthe structure of the input formula to the amount of work which may

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederbe saved by using the proposed optimization. Furthermore,

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederwe compare our tool with other model checkers for conditional logic

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederand finally we discuss to which extent the described

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederoptimization could be used for other modal logics than just

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederconditional logic.

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\section{Coalgebraic conditional logic}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederSome theory here...

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederNeeded from this section: coalgebraic modal logic etc, notion of the set of

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederformulae of a modal logic, provability / satisfiability (weak completeness?

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedersee ~\ref{rem:satProv}).

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederSome (general) words about conditional logic?

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederDaniel to-do-list (in other sections): Memoizing vs. dynamic programming (cite Vardi).

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederComplexity of algorithm(s) (cite lutz+co. paper).

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\section{The algorithm}

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\subsection{The generic sequent calculus}

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederAccording to the introduced framework, we now devise a generic

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederalgorithm to decide the provability of formulae. By

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederinstantiating the generic algorithm to a specific modal logic

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder(simply by using the defining modal rule of this logic), it is

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederpossible to obtain an algorithm to decide provability of

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederformulae of this specific modal logic.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\begin{definition}

389174170e85ad6910b3755ce82e0d896dc8bac1Christian MaederA \emph{Sequent} $\Gamma$ is a set of formulae. If the provability

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maederof a sequent is yet to be decided, it is called an \emph{open sequent}.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederIf the provability of a sequent has allready been shown or refuted,

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederthe sequent is called a \emph{treated sequent}. A \emph{premise}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder$\Lambda$ is a set of open sequents.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\end{definition}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maeder\begin{definition}

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maeder\noindent A \emph{rule} $r=(\Lambda,\Gamma)$ consists of a premise

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maederand an open sequent (usually called \emph{conclusion}).

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maeder\end{definition}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\noindent The generic sequent calculus is given by a set of rules

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder$\mathcal{R}_{sc}$ which consists of the finishing and the branching

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederrules $\mathcal{R}^b_{sc}$ (i.e. rules with no premise or more than

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maederone premise), the linear rules $\mathcal{R}^l_{sc}$ (i.e. rules with

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederexactly one premise) and the modal rule $\mathcal R^m_{sc}$. The

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederfinishing and the branching rules are presented in Figure~\ref{fig:branching}

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maeder(where $\top=\neg\bot$ and $p$ is an atom), the

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederlinear rules are shown in Figure~\ref{fig:linear}. For now, we consider the modal

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederrule $\mathcal R^m_{sc}$ of the standard modal logic \textbf{K}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder(as given by Figure~\ref{fig:modalK}). Note again that

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederit is possible to treat different modal logics with the same generic

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroedercalculus just by appropriately instantiating the modal rule.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\begin{figure}[!h]

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \begin{center}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \begin{tabular}{| c c c |}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \hline

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder & & \\[-5pt]

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (\textsc {$\neg$F}) \inferrule{ }{\Gamma, \neg\bot} &

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (\textsc {Ax}) \inferrule{ }{\Gamma, p, \neg p} &

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (\textsc {$\wedge$}) \inferrule{\Gamma, A \\ \Gamma, B}{\Gamma, A\wedge B} \\[-5pt]

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder & & \\

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \hline

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \end{tabular}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \end{center}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \caption{The finishing and the branching sequent rules $\mathcal{R}^b_{sc}$}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \label{fig:branching}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\end{figure}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maeder\begin{figure}[!h]

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maeder \begin{center}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \begin{tabular}{| c c |}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \hline

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder & \\[-5pt]

389174170e85ad6910b3755ce82e0d896dc8bac1Christian Maeder (\textsc {$\neg\neg$})\inferrule{\Gamma, A}{\Gamma, \neg\neg A} &

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (\textsc {$\neg\wedge$}) \inferrule{\Gamma, \neg A, \neg B}{\Gamma, \neg(A\wedge B)} \\[-5pt]

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder & \\

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \hline

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \end{tabular}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \end{center}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \caption{The linear sequent rules $\mathcal{R}^l_{sc}$}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \label{fig:linear}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{figure}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\begin{figure}[!h]

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \begin{center}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \begin{tabular}{| c |}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \hline

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \\[-5pt]

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (\textsc {\textbf{K}})\inferrule{\neg A_1, \ldots , \neg A_n, A_0}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {\Gamma, \neg \Box A_1,\ldots,\neg \Box A_n, \Box A_0 } \\[-5pt]

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \\

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \hline

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \end{tabular}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \end{center}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \caption{The modal rule of \textbf{K}}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \label{fig:modalK}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\end{figure}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederAlgorithm~\ref{alg:seq} makes use of the sequent rules in the following manner:

1a38107941725211e7c3f051f7a8f5e12199f03acmaederIn order to show the \emph{provability} of a formula $\phi$, the

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederalgorithm starts with the sequent $\{\phi\}$ and tries to apply all

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederof the sequent rules $r\in R_{sc}$ to it

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\footnote{The actual haskell

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimplementation of the algorithm first tries to apply the linear rules

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederfrom $\mathcal{R}^l_{sc}$ and afterwards it tries to apply the other

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederrules from $\mathcal{R}^b_{sc}$ and $\mathcal{R}^m_{sc}$.}.

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder % explain what 'applying' means

1a38107941725211e7c3f051f7a8f5e12199f03acmaederThe result of this one step of application of the rules will be a set

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederof premises $P$. The proving function is then recursively started on

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroedereach sequent of every premise in this set. If there is any premise

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederwhose sequents are all provable, the application of the according rule is

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederjustified and hence the algorithm has succeeded.

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{remark}

389174170e85ad6910b3755ce82e0d896dc8bac1Christian MaederDue to $\ldots$ %what?

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder, the \emph{satisfiability} of a formula $\phi$ amounts to the provability

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederof its negation $\neg \phi$.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\label{rem:satProv}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{remark}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{algorithm}[h]

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\begin{alg}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{upshape}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Step 1: Take the input formula $\phi$, construct the initial open

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder sequent $\Gamma_0 = \{\phi\}$ from it. Set i=0.\\

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Step 2: Try to apply all rules $r\in R_{sc}$ to any open sequent

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder $\Gamma_i$. Let $\Lambda_i$ denote the set of the resulting open

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder premises.\\

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Step 3: If $\Lambda_i$ contains the empty premise, mark the open

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder sequent $\Gamma_i$ as proven. If $\Lambda_i$ contains no premise at

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder all, mark the open sequent $\Gamma_i$ as refuted.\\

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Step 4: Else, add all premises from $\Lambda_i$ to the set of open

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder premises and choose any premise from this set. Add all $\Gamma^j_i$

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder from this premise to the set of open sequents and continue with

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Step 2.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\end{upshape}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\label{alg:seq}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{alg}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{algorithm}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{proposition}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\begin{upshape}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederAlgorithm~\ref{alg:seq} is sound and complete w.r.t. provability. Furthermore,

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederAlgorithm~\ref{alg:seq} has complexity X.

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{upshape}

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder\end{proposition}

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder\begin{proof}

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder...

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{proof}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\subsection{The conditional logic instance}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederThe genericity of the introduced sequent calculus allows us to easiliy

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedercreate instantiations of Algorithm~\ref{alg:seq} for a large variety

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederof modal logics:

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederBy setting $\mathcal R^m_{sc}$ for instance to the rule shown in

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederFigure~\ref{fig:modalCKCEM}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder(where $A_a = A_b$ is shorthand for $A_a\rightarrow A_b\wedge A_b\rightarrow A_a$), we

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederobtain an algorithm for deciding provability (and satisfiability) of

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederconditional logic. Note however, that we restrict ourselves to the

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederexamplary conditional logic \textbf{CKCEM} for the remainder of this section

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder(slightly adapted versions of the optimization will work for other conditional logics).

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\begin{figure}[h!]

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \begin{center}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \begin{tabular}{| c |}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \hline

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \\[-5pt]

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (\textsc {\textbf{CKCEM}})\inferrule{A_0 = \ldots = A_n \\ B_0,\ldots, B_j,\neg B_{j+1},\ldots,\neg B_n}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder {\Gamma, (A_0\Rightarrow B_0),\ldots,(A_j\Rightarrow B_j),

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \neg(A_{j+1}\Rightarrow B_{j+1}),\ldots,\neg(A_n\Rightarrow B_n) } \\[-5pt]

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \\

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \hline

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \end{tabular}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \end{center}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \caption{The modal rule $\textbf{CKCEM}$ of conditional logic}

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder \label{fig:modalCKCEM}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\end{figure}

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederIn the following, we use the notions of \emph{conditional antecedent} and

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder\emph{conditional consequent} to refer to the parameters of the modal operator of

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederconditional logic.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederIn order to decide whether there is an

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederinstance of the modal rule of conditional logic which can be applied to

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederthe actual current sequent, it is necessary to create a preliminary premise

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederfor each possible combination of equalities of all the premises of the

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedermodal operators in this sequent. This results in $2^n$ new premises for

b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedera sequent with $n$ top-level modal operators.

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder

ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder\begin{example}

Consider the sequent $\Gamma=\{(A_0\Rightarrow B_0),(A_1\Rightarrow B_1),

(A_2\Rightarrow B_2)\}$. By instantiating the modal rule, several

new premises

such as $\{\{A_0=A_1=A_2\},\{B_0,B_1,B_2\}\}$ or $\{\{A_0=A_2\},\{B_0,B_2\}\}$

may be obtained. Only after the equalities in the first sequent of each

of these premises have been shown (or refuted), it is clear whether the

current instantiation of the modal rule is actually leading to a possibly

provable premise.

\label{ex:cond}

\end{example}

It seems to be a more intelligent approach to first

partition the set of all antecedents of the top-level modal operators in the

current sequent into equivalence classes with respect to logical equality.

This partition does not only allow for a reduction of the number of newly

created open premises in each modal step,

but it also allows us to seperate the two parts of the conditional modal step

(i.e. the first part, showing the necessary equalities, and the second

part, showing that the resulting sequent - consisting only of the appropriate

conditional consequences - is actually provable itself).

\begin{example}

Consider again the sequent from Example~\ref{ex:cond}. By using the examplary

knowledge, that $A_0=A_1$, $A_1\neq A_2$ and $A_0\neq A_2$, it is immediate,

that there are just two reasonable instations of the modal rule, leading

to the two premises $\{\{B_0,B_1\}\}$ and $\{\{B_2\}\}$. For the

first of these two premises, note that it is not necessary to show the

equivalence of $A_0$ and $A_1$ again.

\end{example}

\begin{remark}

In the case of conditional logic, observe the following: Since the

modal antecedents that appear in a formula are not being changed by any

rule of the sequent calculus, it is possible to extract all possibly

relevant antecedents of a formula even \emph{before} the actual sequent

calculus iswe applied. This allows us to first compute the equivalence

classes of all the relevant antecedents and then feed this knowledge into

the actual sequent calculus:

\end{remark}

\section{The optimization}

\begin{definition}

A conditional antecedent of \emph{modal nesting depth} $i$ is a

conditional antecedent which contains at least one antecedent of

modal nesting depth $i-1$ and which contains no antecedent

of modal nesting depth greater than $i-1$. A

conditional antecedent of nesting depth 0 is an antecedent

that does not contain any further modal operators.

Let $p_i$ denote the set of all conditional antecedents of modal

nesting depth $i$. Further, let $prems(n)$ denote the set of all

conditional antecedents of modal nesting depth at most $n$ (i.e.

$prems(n)=\bigcup_{j=1..n}^{} p_j$).

Finally, let $depth(\phi)$ denote the maximal modal nesting in

the formula $\phi$.

\end{definition}

\begin{example}

In the formula $\phi=((p_0\Rightarrow p_1) \wedge ((p_2\Rightarrow p_3)\Rightarrow p_4))

\Rightarrow (p_5\Rightarrow p_6)$,

the premise $((p_0\Rightarrow p_1) \wedge ((p_2\Rightarrow p_3)\Rightarrow p_4))$ has a

nesting depth of 2 (and not 1), $(p_0\Rightarrow p_1)$ and $(p_2\Rightarrow p_3)$ both

have a nesting depth of 1, and finally $p_0$, $p_2$ and $p_4$ all have a nesting depth of 0.

Furthermore, $prems(1)=\{p_0,p_2,p_4,(p_0\Rightarrow p_1),(p_2\Rightarrow p_3)\}$

and $depth(\phi)=3$.

\end{example}

\begin{definition}

A set $\mathcal{K}$ of treated sequents together with a function

$eval:\mathcal{K}\rightarrow \{\top,\bot\}$ is called \emph{knowledge}.

\end{definition}

We may now construct an optimized algorithm which may allow us

to decide provability (and satisfiability) of formulae more efficiently

in some cases. The optimized algorithm is constructed from two functions

(namely from the so-called \emph{pre-proving} function and the actual proving

function):

\begin{algorithm}[h]

\begin{alg}

\begin{upshape}

Step 1: Take a formula $\phi$ and knowledge $(\mathcal{K},eval)$ as

input. Set $\Gamma_0 = \{\phi\}$, $i=0$.\\

Step 2: Try to apply all rules $r\in \mathcal{RO}_{sc}$

(supplying $\mathcal{RO}^m_{sc}$ with knowledge $(\mathcal{K},eval)$)

to any open sequent $\Gamma_i$. Let

$\Lambda_i$ denote the set of the resulting premises.\\

Step 3: If $\Lambda_i$ contains the empty premise, mark the open

sequent $\Gamma_i$ as proven. If $\Lambda_i$ contains no premise at

all, mark the open sequent $\Gamma_i$ as refuted.\\

Step 4: Else, add all premises from $\Lambda_i$ to the set of open

premises and choose any premise from this set. Add all $\Gamma^j_i$

from this premise to the set of open sequents and continue with

Step 2.

\label{alg:optSeq}

\end{upshape}

\end{alg}

\end{algorithm}

Algorithm~\ref{alg:optSeq} is very similar to Algorithm~\ref{alg:seq},

however, it uses a modified

set of rules $\mathcal{RO}_{sc}$ and it also allows for the

input of some knowledge $(\mathcal{K},eval)$ in the form of a set of sequents

together with an evaluation function. This knowledge is passed on to

the modified modal rule of conditional logic, which makes appropriate use of it.

$\mathcal{RO}_{sc}$ is obtained from $\mathcal{R}_{sc}$ by replacing

the modal rule from Figure~\ref{fig:modalCKCEM} with the modified modal

rule from Figure~\ref{fig:modalCKCEMm}.

\begin{figure}[h!]

\begin{center}

\begin{tabular}{| c |}

\hline

\\[-5pt]

(\textsc {\textbf{CKCEM}$^m$})\inferrule{\bigwedge{}_{i,j=\{1..n\}}{eval(A_i=B_j)=\top}

\\ B_0,\ldots, B_j,\neg B_{j+1},\ldots,\neg B_n}

{\Gamma, (A_0\Rightarrow B_0),\ldots,(A_j\Rightarrow B_j),

\neg(A_{j+1}\Rightarrow B_{j+1}),\ldots,\neg(A_n\Rightarrow B_n) } \\[-5pt]

\\

\hline

\end{tabular}

\end{center}

\caption{The modified modal rule \textbf{CKCEM}$^m$ of conditional logic}

\label{fig:modalCKCEMm}

\end{figure}

\begin{algorithm}[h]

\begin{alg}

\begin{upshape}

Step 1: Take a formula $\phi$ as input. Set $i=0$, $\mathcal{K}_0=\emptyset$, $eval_0=\emptyset$.\\

Step 2: Generate the set $prems_i$ of all conditional antecedents of $\phi$

of nesting depth at most $i$. If $i<depth(\phi)$ continue

with Step 3, else set $\mathcal{K}=\mathcal{K}_{i-1}, eval=eval_{i-1}$ and continue with Step 4.\\

Step 3: Let $eq_i$ denote the set of all equalities $A_a = A_b$ for different

formulae $A_a,A_b\in prems_i$. Compute

Algorithm~\ref{alg:optSeq} ($\psi$, $(\mathcal{K}_i,eval_i)$) for all $\psi\in eq_i$.

Set $\mathcal{K}_{i+1} = eq_i$, set $i = i + 1$. For each equality $\psi\in eq_i$,

set $eval_{i+1}(\psi)=\top$ if the result of Algorithm~\ref{alg:optSeq} was \verb+True+

and $eval_{i+1}(\psi)=\bot$ otherwise. Continue with Step 2.\\

Step 4: Call Algorithm~\ref{alg:optSeq} ($\phi$, $(\mathcal{K},eval)$).

\label{alg:preprove}

\end{upshape}

\end{alg}

\end{algorithm}

Algorithm~\ref{alg:preprove} first computes the knowledge $(\mathcal{K},eval)$ about specific

subformulae of $\phi$ and then finally checks for provability of

$\phi$ (using this knowledge): In order to show the equivalence of

two conditional antecedents of nesting depth at most $i$, we assume,

that the equalities $\mathcal{K}_{i}$ between modal antecedents of nesting depth less

than $i$ have allready been computed and the result is stored in $eval_i$; hence,

two antecedents are equal, if their equivalence is provable by

Algorithm~\ref{alg:optSeq} using only the knowledge $(\mathcal{K}_{i},eval_i)$.

\subsection{Treatment of needed equivalences only}

Since Algorithm~\ref{alg:preprove} tries to show the logical equivalence of every combination

of any two conditional antecedents that appear in $\phi$, it will have worse completion

time than Algorithm~\ref{alg:seq} on many formulae:

\begin{example}

Consider the formula

\begin{quote}

$\phi=(((p_0\Rightarrow p_1)\Rightarrow p_2)\Rightarrow p_4)\vee

(((p_5\Rightarrow p_6)\Rightarrow p_7)\Rightarrow p_8)$.

\end{quote}

Algorithm~\ref{alg:preprove} will not only

try to show the necessary equivalences between the pairs

$(((p_0\Rightarrow p_1)\Rightarrow p_2), ((p_5\Rightarrow p_6)\Rightarrow p_7))$,

$((p_0\Rightarrow p_1), (p_5\Rightarrow p_6))$ and $(p_0,p_5)$, but it will

also try to show equivalences between any two conditional antecedents (e.g. $(p_0,

(p_5\Rightarrow p_6))$), even though these equivalences may not be needed

during the execution of Algorithm~\ref{alg:optSeq}.

\end{example}

Based on this observation, it is possible to assign a category to each pair of

antecedents that appear in it:

\begin{definition}

Two conditional antecedents $A$ and $B$ are called \emph{connected (in $\phi$)} if

they both are the antecedent of a top-level modality.

Furthermore, we define sub-antecedents $C$ and $D$ of connected antecedents $A$ and $B$

to be connected to each other, if they appear at the same position in a chain

of conditional antecedents (formally: $A=(\ldots(C\Rightarrow a_n)\ldots \Rightarrow a_0)$,

$B=(\ldots(D\Rightarrow b_n)\ldots \Rightarrow b_0)$).

Two conditional antecedents $A$ and $B$ are called \emph{independent (in $\phi$)} if

they occur at a different modal depth (even though they may have modal nestings the same depth).

The relevance of two antecedents with regard to each other is said to be

\emph{pending} if they occur at the same depth in $\phi$ but each

in the consequent of a different modal operator.

\end{definition}

Since two independent antecedents will never appear in the scope of the

same application of the modal rule, it is in no case necessary to show (or

refute) the logical equivalence of independent

conditional antecedents. Hence it suffices to focus

our attention to the connected and pending conditional antecedents. By pre-proving only

the equivalences of the connected antecedents, we can be assured that we are

always as efficient as Algorithm~\ref{alg:optSeq}. However, it would still

be necessary to treat the equivalence of those initially pending antecedents which

turn out to be connected during the execution of Algorithm~\ref{alg:optSeq}.

This would not allow us to completely seperate to treatment of equivalences

(achieved by Algorithm~\ref{alg:preprove}) and the actual sequent calculus (realized by

Algorithm~\ref{alg:optSeq}).

If the pending antecedents are also included in the pre-proving, it is obvious, that

any possibly needed equivalence and its truth-value are allready included in $(K,eval)$

when the main proving is induced. On the other hand, we have to be aware that it

may be the case, that we show equivalences of antecedents which later turn out to

be independent.

As result of these considerations, we devise Algorithm~\ref{alg:optPreprove},

an improved version of Algorithm~\ref{alg:preprove}. The only difference is

that before proving any equivalence, Algorithm~\ref{alg:optPreprove} checks

whether the current pair of conditional antecedents is actually connected or if their

relevance to each other is pending; only then it treats the equivalence. Hence

independent pairs of antecedents remain untreated.

\begin{algorithm}[h]

\begin{alg}

\begin{upshape}

Step 1: Take a formula $\phi$ as input. Set $i=0$, $\mathcal{K}_0=\emptyset$, $eval_0=\emptyset$.\\

Step 2: Generate the set $prems_i$ of all conditional antecedents of $\phi$

of nesting depth at most $i$. If $i<depth(\phi)$ continue

with Step 3, else set $\mathcal{K}=\mathcal{K}_{i-1}, eval=eval_{i-1}$ and continue with Step 4.\\

Step 3: Let $eq_i$ denote the set of all equalities $A_a = A_b$ for different and not independent

pairs of formulae $A_a,A_b\in prems_i$. Compute

Algorithm~\ref{alg:optSeq} ($\psi$, $(\mathcal{K}_i,eval_i)$) for all $\psi\in eq_i$.

Set $\mathcal{K}_{i+1} = eq_i$, set $i = i + 1$. For each equality $\psi\in eq_i$,

set $eval_{i+1}(\psi)=\top$ if the result of Algorithm~\ref{alg:optSeq} was \verb+True+

and $eval_{i+1}(\psi)=\bot$ otherwise. Continue with Step 2.\\

Step 4: Call Algorithm~\ref{alg:optSeq} ($\phi$, $(\mathcal{K},eval)$).

\label{alg:optPreprove}

\end{upshape}

\end{alg}

\end{algorithm}

\begin{proposition}

\begin{upshape}

Algorithm~\ref{alg:optPreprove} is sound and complete w.r.t. provability.

Algorithm~\ref{alg:optPreprove} has complexity X. Furthermore, Algorithm~\ref{alg:optPreprove}

allows us, to completely seperate the pre-proving of equivalences and

the actual sequent calculus.

\end{upshape}

\end{proposition}

\begin{proof}

...

\end{proof}

\section{Generalized optimization}

As previously mentioned, the demonstrated optimization is not restricted to the

case of conditional

modal logics.

\begin{definition}

If $\Gamma$ is a sequent, we denote the set of all arguments of

top-level modalities from $\Gamma$ by $arg(\Gamma)$.

A \emph{short sequent} is a sequent which consists of just one formula which

itself is a propositional formula over a fixed maximal number of modal arguments

from $arg(\Gamma)$. In the following, we fix the maximal number of modal arguments

in short sequents to be 2.

\end{definition}

The general method of the optimization then takes the following form:

Let $S_1,\ldots S_n$ be short sequents and assume that there is

a (w.r.t the considered modal logic) sound instance of the generic rule which

is depicted in Figure~\ref{fig:modalOpt} (where $\mathcal{S}$ is a set of any

sequents).

\begin{figure}[!h]

\begin{center}

\begin{tabular}{| c |}

\hline

\\[-5pt]

(\textsc {\textbf{Opt}}) \inferrule{ S_1 \\ \ldots \\ S_n \\ \mathcal{S} }

{ \Gamma } \\[-5pt]

\\

\hline

\end{tabular}

\end{center}

\caption{The general rule-scheme to which the optimization may be applied}

\label{fig:modalOpt}

\end{figure}

We are now able to devise a final version (Algorithm~\ref{alg:genOptPreprove}) of the

optimized algorithm: Instead of considering only equivalences of conditional antecedents

for pre-proving, we now extend our attention to any short sequents over any modal arguments.

\begin{algorithm}[h]

\begin{alg}

\begin{upshape}

Step 1: Take a formula $\phi$ as input. Set $i=0$, $\mathcal{K}_0=\emptyset$, $eval_0=\emptyset$.\\

Step 2: Generate the set $args_i$ of all modal arguments of $\phi$

which have nesting depth at most $i$. If $i<depth(\phi)$ continue

with Step 3, else set $\mathcal{K}=\mathcal{K}_{i-1}, eval=eval_{i-1}$ and continue with Step 4.\\

Step 3: Let $seq_i$ denote the set of all short sequents $S_1$ over at most two formulae

$A_a,A_b\in args_i$. Compute Algorithm~\ref{alg:optSeq} ($\psi$, $(\mathcal{K}_i,eval_i)$) for all

$\psi\in seq_i$. Set $\mathcal{K}_{i+1} = seq_i$, set $i = i + 1$. For each short sequent

$\psi\in seq_i$, set $eval_{i+1}(\psi)=\top$ if the result of Algorithm~\ref{alg:optSeq} was

\verb+True+ and $eval_{i+1}(\psi)=\bot$ otherwise. Continue with Step 2.\\

Step 4: Call Algorithm~\ref{alg:optSeq} ($\phi$, $(\mathcal{K},eval)$).

\end{upshape}

\label{alg:genOptPreprove}

\end{alg}

\end{algorithm}

Thus it is valid to use this new Algorithm~\ref{alg:genOptPreprove} where the employed ruleset has to be

extended by the generic modified rule given by Figure~\ref{fig:modModalOpt}.

\begin{figure}[!h]

\begin{center}

\begin{tabular}{| c |}

\hline

\\[-5pt]

(\textsc {\textbf{Opt}$^m$}) \inferrule{ eval(S_1)=\top \\ \ldots \\ eval(S_n)=\top \\ \mathcal{S} }

{ \Gamma } \\[-5pt]

\\

\hline

\end{tabular}

\end{center}

\caption{The general optimized rule}

\label{fig:modModalOpt}

\end{figure}

\begin{example}

The following two cases are may be instances of the generic optimization:

\begin{enumerate}

\item (Classical modal Logics / Neighbourhood Semantics) Let $\Gamma = \{\Box A = \Box B\}$,

$n=1$, $S_1=\{A=B\}$ and $\mathcal{S}=\emptyset$. Algorithm~\ref{alg:genOptPreprove}

may be then applied whenever the following congruence rule is sound in the considered

logic:

\begin{quote}

\begin{center}

(\textsc {\textbf{Opt}$_{Cong}$}) \inferrule{ A=B }

{ \Box A = \Box B }

\end{center}

\end{quote}

The according modified version of this rule is as follows:

\begin{quote}

\begin{center}

(\textsc {\textbf{Opt}$^m_{Cong}$}) \inferrule{ {eval(A=B)=\top} }

{ \Box A = \Box B }

\end{center}

\end{quote}

\item (Monotone modal logics) By setting $\Gamma = \{\Box A \rightarrow \Box B\}$,

$n=1$, $S_1=\{A\rightarrow B\}$ and $\mathcal{S}=\emptyset$, we may instantiate

the generic algorithm to the case of modal logics which are monotone w.r.t. their

modal operator. So assume the following rule to be sound in the considered modal

logic:

\begin{quote}

\begin{center}

(\textsc {\textbf{Opt}$_{Mon}$}) \inferrule{ A\rightarrow B }

{ \Box A \rightarrow \Box B }

\end{center}

\end{quote}

The according modified version of this rule is as follows:

\begin{quote}

\begin{center}

(\textsc {\textbf{Opt}$^m_{Mon}$}) \inferrule{ {eval(A\rightarrow B)=\top} }

{ \Box A \rightarrow \Box B }

\end{center}

\end{quote}

In the case, that \textbf{Opt}$_{Mon}$ is the only modal rule in the

considered logic (i.e. the case of plain monotone modal logic), all the

prove-work which is connected to the modal operator is shifted to the

pre-proving process. Especially matching with the modal rules

$\mathcal{RO}^m_{sc}$ becomes a mere lookup of the value of $eval$.

This means, that all calls of the sequent algorithm Algorithm~\ref{alg:optSeq}

correspond in complexity just to ordinary sat-solving of propositional logic.

Furthermore, Algorithm~\ref{alg:optSeq} will be called $|\phi|$ times. This

observation may be generalized:

\end{enumerate}

\label{ex:neighMon}

\end{example}

\begin{remark}

In the case that all modal rules of the considered logic are instances of

the generic rule (\textbf{Opt}) with $P=\emptyset$ (as seen in Example~\ref{ex:neighMon}),

the optimization does not only allow for a reduction of computing time, but

it also allows us to effectively reduce the sequent calculus to a sat-solving

algorithm.

Furthermore, the optimized algorithm will always be as efficient as the

original one in this case (since every occurence of short sequents over $arg(\Gamma)$

which accord to the current instantiation of the rule (\textbf{Opt}) will

have to be shown or refuted even during the course of the original algorithm).

\end{remark}

\section{Implementation}

The proposed optimized algorithms have been implemented as part of the

generic coalgebraic modal logic satisfiability solver (CoLoSS). CoLoSS provides

the general coalgebraic framework in which a generic sequent calculus is

embedded. It is easily possible to instantiate this generic sequent calculus to

specific modal logics, one particular example being conditional logic. The CoLoSS matching

function for conditional logic was hence adapted in order to realize the different

optimizations, so that CoLoSS now provides an efficient

Write a few words about the Haskell-Implementation here. Nothing interresting apart

from the Web-Interface, and that all of this is a part of CoLoSS.

\subsection{Comparing the proposed algorithms}

In order to show the relevance of the proposed optimizations, we devise three classes

of conditional formulae. Each class has a characteristic general shape, establishing its

difficulty w.r.t. the different algorithms:

Let $p_i$ denote atoms in the following.

\begin{itemize}

\item The formula \verb|bloat(|$i$\verb|)| is a full binary tree of depth $i$ (containing $2^i$ pairwise logically

inqevuilant atoms and $2^i-1$ modal antecedents):

\begin{quote}

\verb|bloat(|$i$\verb|)| = $($\verb|bloat(|$i-1$\verb|)|$)\Rightarrow($\verb|bloat(|$i-1$\verb|)|)\\

\verb|bloat(|$0$\verb|)| = $p_{rand}$

\end{quote}

Formulae from this class should show the problematic perfomance of Algorithm~\ref{alg:preprove} whenever

a formula contains many modal antecedents which appear at different depths. Since Algorithm~\ref{alg:preprove}

does not check whether pairs of modal antecedents are independent or connected, it should perform considerably worse

than Algorithm~\ref{alg:optPreprove} which only attempts to prove the logical equivalence of formulae which are not

independent. A comparison of the different algorithms w.r.t. formulae \verb|bloat(|$i$\verb|)| is depicted in

Figure~\ref{fig:benchBloat}.

\item The formula \verb|conjunct(|$i$\verb|)| is just an $i$-fold conjunction of a specific formula $A$:

\begin{quote}

\verb|conjunct(|$i$\verb|)| = $A_1\wedge\ldots\wedge A_i$\\

$A=(((p_1\vee p_0)\Rightarrow p_2)\vee((p_0\vee p_1)\Rightarrow p_2))\vee\neg(((p_0\vee p_1)\Rightarrow p_2)\vee((p_1\vee p_0)\Rightarrow p_2))$)

\end{quote}

This class contains formulae which contain logically (but not sytactically!) equivalent antecedents.

As $i$ increases, so does the amount of appearance of identical modal antecedents in different positions

of the considered formula. Hence the optimized should perform considerably better than the unoptimized

Algorithm~\ref{alg:seq}. A comparison of the different algorithms w.r.t. formulae \verb|conjunct(|$i$\verb|)| is depicted in

Figure~\ref{fig:benchConjunct}.

\item The formula \verb|explode(|$i$\verb|)| contains equivalent but not syntactically

equal and interchangingly nested modal antecedents of depth at most $i$:

\begin{quote}

\verb|explode(|$i$\verb|)| = $X^i_1\vee\ldots\vee X^i_i$\\

$X^i_1=(A^i_1\Rightarrow(\ldots(A^i_i\Rightarrow (c_1\wedge\ldots\wedge c_i))\ldots))$\\

$X^i_j=(A^i_{j\bmod i}\Rightarrow(\ldots(A^i_{(j+(i-1))\bmod i}\Rightarrow \neg c_j)\ldots))$\\

$A^i_j=p_{j \bmod i}\wedge p_{(j+(i-1)) \bmod i}$

\end{quote}

This class contains complex formulae for which the unoptimized algorithm should not be

efficient any more: Only the combined knowledge about all appearing modal antecedent allows

the proving algorithm to reach all conclusions $c_i$, and only the combined sequent

$(c_1\wedge\ldots\wedge c_i),\neg c_1,\ldots,\neg c_i$ (containing every appearing

conclusion) is provable. The algorithms perform as expected (see Figure~\ref{fig:benchExplode}).

\end{itemize}

\begin{figure}[!h]

\begin{center}

\begin{tabular}{| l | r | r | r |}

\hline

$i$ & Algorithm~\ref{alg:seq} & Algorithm~\ref{alg:preprove} & Algorithm~\ref{alg:optPreprove} \\

\hline

1 & 0,008s & 0,009s & 0,010s\\

2 & 0,008s & 0,011s & 0,010s\\

3 & 0,009s & 0,028s & 0,014s\\

4 & 0,010s & 0,233s & 0,022s\\

5 & 0,011s & 2,840s & 0,087s\\

6 & 0,013s & 33,476s & 0,590s\\

7 & 0,019s & 402,239s & 4,989s\\

\hline

\end{tabular}

\end{center}

\caption{Results for bloat($i$)}

\label{fig:benchBloat}

\end{figure}

\begin{figure}[!h]

\begin{center}

\begin{tabular}{| l | r | r | r |}

\hline

$i$ & Algorithm~\ref{alg:seq} & Algorithm~\ref{alg:preprove} & Algorithm~\ref{alg:optPreprove} \\

\hline

1 & 0,012s & 0,013s & 0,012s\\

2 & 0,021s & 0,015s & 0,014s\\

3 & 0,681s & 0,021s & 0,021s\\

4 & 131,496s & 0,048s & 0,048s\\

5 & $>$600,000s & 0,199s & 0,201s\\

6 & $>>$600,000s & 1,152s & 1,161s\\

7 & $>>$600,000s & 8,746s & 8,667s\\

8 & $>>$600,000s & 74,805s & 75,595s\\

9 & $>>$600,000s & 730,589s & 742,357s\\

\hline

\end{tabular}

\end{center}

\caption{Results for conjunct($i$)}

\label{fig:benchConjunct}

\end{figure}

\begin{figure}[!h]

\begin{center}

\begin{tabular}{| l | r | r | r |}

\hline

$i$ & Algorithm~\ref{alg:seq} & Algorithm~\ref{alg:preprove} & Algorithm~\ref{alg:optPreprove} \\

\hline

1 & 0,009s & 0,008s & 0,009s\\

2 & 0,011s & 0,010s & 0,010s\\

3 & 0,028s & 0,012s & 0,014s\\

4 & 0,268s & 0,018s & 0,018s\\

5 & 4,555s & 0,025s & 0,027s\\

6 & 10,785s & 0,035s & 0,039s\\

7 & $>>$600,000s & 0,054s & 0,060s\\

8 & $>>$600,000s & 0,079s & 0,089s\\

9 & $>>$600,000s & 0,122s & 0,140s\\

\hline

\end{tabular}

\end{center}

\caption{Results for explode($i$)}

\label{fig:benchExplode}

\end{figure}

The tests reveal that a significant increase of performance may be obtained through

the proposed

optimizations. In general, the implementation of the proposed algorithms (realized

in CoLoSS) has a comparable performance to

other conditional logic provers (such as CondLean). However, the authors of other

provers did not publish their benchmarking sets of formulae, so that a direct

comparison was not possible. Since other provers do not implement the optimization

strategies proposed in this paper, it is reasonable to assume, that the optimized

implementation in CoLoSS outperforms other systems at least for the

considered examplary formulae \verb|explode(|i\verb|)| and \verb|conjunct(|i\verb|)|.

\section{Summary}

\begin{problem}

Finish your paper and get it to your Program Chairman on time!

\end{problem}

\section{Bibliographical references}\label{references}

\begin{thebibliography}{10}\label{bibliography}

\bibitem{cy} Civin, P., and B. Yood, \emph{Involutions on Banach

algebras}, Pacific J. Math. \textbf{9} (1959), 415--436.

\end{thebibliography}

\end{document}