c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder\documentclass{entcs} \usepackage{entcsmacro}

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder\usepackage{graphicx}

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder\usepackage{mathpartir}

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder\usepackage{amsmath,amssymb}

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder\newcommand{\hearts}{\heartsuit}

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder\newcommand{\prems}{\mathit{prems}}

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder\newcommand{\eval}{\mathit{eval}}

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder\input{header}

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder\sloppy

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder% The following is enclosed to allow easy detection of differences in

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder% ascii coding.

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski% 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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski% 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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski% Digits 0 1 2 3 4 5 6 7 8 9

af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski% Exclamation ! Double quote " Hash (number) #

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski% Dollar $ Percent % Ampersand &

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski% Acute accent ' Left paren ( Right paren )

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% Asterisk * Plus + Comma ,

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder% Minus - Point . Solidus /

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% Colon : Semicolon ; Less than <

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% Equals =3D Greater than > Question mark ?

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% At @ Left bracket [ Backslash \

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% Right bracket ] Circumflex ^ Underscore _

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% Grave accent ` Left brace { Vertical bar |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% Right brace } Tilde ~

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% A couple of exemplary definitions:

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder%\newcommand{\Nat}{{\mathbb N}}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder%\newcommand{\Real}{{\mathbb R}}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder\newcommand{\COLOSS}{{\textrm CoLoSS}}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder\def\lastname{Hausmann and Schr\"oder}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder\begin{document}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\begin{frontmatter}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \title{Optimizing Conditional Logic Reasoning within \COLOSS}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \author[DFKI]{Daniel Hausmann\thanksref{myemail}}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \author[DFKI,UBremen]{Lutz Schr\"oder\thanksref{coemail}}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \address[DFKI]{DFKI Bremen, SKS}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \address[UBremen]{Department of Mathematics and Computer Science, Universit\"at Bremen, Germany}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder% \thanks[ALL]{Work forms part of DFG-project \emph{Generic Algorithms and Complexity

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder% Bounds in Coalgebraic Modal Logic} (SCHR 1118/5-1)}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \thanks[myemail]{Email: \href{mailto:Daniel.Hausmann@dfki.de} {\texttt{\normalshape Daniel.Hausmann@dfki.de}}}

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

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder\begin{abstract}

63324a97283728a30932828a612c7b0b0f687624Christian Maeder The generic modal reasoner CoLoSS covers a wide variety of logics

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder ranging from graded and probabilistic modal logic to coalition logic

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder and conditional logics, being based on a broadly applicable

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder coalgebraic semantics and an ensuing general treatment of modal

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sequent and tableau calculi. Here, we present research into

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder optimisation of the reasoning strategies employed in

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder CoLoSS. Specifically, we discuss strategies of memoisation and

63324a97283728a30932828a612c7b0b0f687624Christian Maeder dynamic programming that are based on the observation that short

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sequents play a central role in many of the logics under

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski study. These optimisations seem to be particularly useful for the

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder case of conditional logics, for some of which dynamic programming

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski even improves the theoretical complexity of the algorithm. These

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski strategies have been implemented in CoLoSS; we give a detailed

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comparison of the different heuristics, observing that in the

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski targeted domain of conditional logics, a substantial speed-up can be

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder achieved.

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski\end{abstract}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski\begin{keyword}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Coalgebraic modal logic, conditional logic, automated reasoning,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski optimisation, heuristics, memoizing, dynamic programming

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski\end{keyword}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski\end{frontmatter}

3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder\section{Introduction}\label{intro}

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescuIn recent decades, modal logic has seen a development towards semantic

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescuheterogeneity, witnessed by an emergence of numerous logics that,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiwhile still of manifestly modal character, are not amenable to

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskistandard Kripke semantics. Examples include probabilistic modal

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskilogic~\cite{FaginHalpern94}, coalition logic~\cite{Pauly02}, and

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiconditional logic~\cite{Chellas80}, to name just a few. The move

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskibeyond Kripke semantics, mirrored on the syntactical side by the

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskifailure of normality, entails additional challenges for tableau and

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskisequent systems, as the correspondence between tableaus and models

bba825b39570777866d560bfde3807731131097eKlaus Luettichbecomes looser, and in particular demands created by modal formulas

bba825b39570777866d560bfde3807731131097eKlaus Luettichcan no longer be discharged by the creation of single successor nodes.

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiThis problem is tackled on the theoretical side by introducing the

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maedersemantic framework of coalgebraic modal

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskilogic~\cite{Pattinson03,Schroder05}, which covers all logics mentioned

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskiabove and many more. It turns out that coalgebraic modal logic does

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederallow the design of generic reasoning algorithms, including a generic

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maedertableau method originating from~\cite{SchroderPattinson09}; this

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maedergeneric method may in fact be separated from the semantics and

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskideveloped purely syntactically, as carried out

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiin~\cite{PattinsonSchroder08b,PattinsonSchroder09a}.

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaederGeneric tableau algorithms for coalgebraic modal logics, in particular

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maederthe algorithm described in~\cite{SchroderPattinson09}, have been

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maederimplemented in the reasoning tool

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder\COLOSS~\cite{CalinEA09}\footnote{available under

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder \url{http://www.informatik.uni-bremen.de/cofi/CoLoSS/}}. As

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maederindicated above, it is a necessary feature of the generic tableau

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maedersystems that they potentially generate multiple successor nodes for a

63324a97283728a30932828a612c7b0b0f687624Christian Maedergiven modal demand, so that in addition to the typical depth problem,

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuproof search faces a rather noticeable problem of breadth. The search

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescufor optimisation strategies to increase the efficiency of reasoning

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuthus becomes all the more urgent. Here we present one such strategy,

b4e202184f6977662c439c82866fe93f06cebe41Christian Maederwhich is generally applicable, but particularly efficient in reducing

830e14495f9cac8e154dd4813dae010166f33d09Mihai Codescuboth depth and branching for the class of conditional logics. We

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuexploit a notable feature of this class, namely that many of the

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescurelevant rules rely rather heavily on premises stating equivalence

f2c050360525df494e6115073b0edc4c443a847cMihai Codescubetween formulas; thus, conditional logics are a good candidate for

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maedermemoising strategies, applied judiciously to short sequents. We

f2c050360525df494e6115073b0edc4c443a847cMihai Codescudescribe the implementation of memoising and dynamic programming

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maederstrategies within \COLOSS, and discuss the outcome of various

f2c050360525df494e6115073b0edc4c443a847cMihai Codescucomparative experiments.

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski\section{Generic Sequent Calculi for Coalgebraic Modal Logic}

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiCoalgebraic modal logic, originally introduced as a specification

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederlanguage for coalgebras, seen as generic reactive

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedersystems~\cite{Pattinson03}, has since evolved into a generic framework

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederfor modal logic beyond Kripke semantics~\cite{CirsteaEA09}. The basic

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederidea is to encapsulate the branching type of the systems relevant for

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederthe semantics of a particular modal logic, say probabilistic or

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedergame-theoretic branching, in the choice of a set functor, the

da955132262baab309a50fdffe228c9efe68251dCui Jiansignature functor (e.g.\ the distribution functor and the games

da955132262baab309a50fdffe228c9efe68251dCui Jianfunctor in the mentioned examples), and to capture the semantics of

bba825b39570777866d560bfde3807731131097eKlaus Luettichmodal operators in terms of so-called predicate liftings. For the

da955132262baab309a50fdffe228c9efe68251dCui Jianpurposes of the present work, details of the semantics are less

bba825b39570777866d560bfde3807731131097eKlaus Luettichrelevant than proof-theoretic aspects, which we shall recall

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederpresently. The range of logics covered by the coalgebraic approach is

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederextremely broad, including, besides standard Kripke and neighbourhood

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedersemantics, e.g.\ graded modal logic~\cite{Fine72}, probabilistic modal

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederlogic~\cite{FaginHalpern94}, coalition logic~\cite{Pauly02}, various

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederconditional logics equipped with selection function

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedersemantics~\cite{Chellas80}, and many more.

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederSyntactically, logics are parametrised by the choice of a \emph{modal

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder similarity type} $\Lambda$, i.e.\ a set of modal operators with

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederassociated finite arities. This choice determines the set of formulas

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder$\phi,\psi$ via the grammar

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder\begin{equation*}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder \phi, \psi ::= p \mid

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder \phi \land \psi \mid \lnot \phi \mid \hearts(\phi_1, \dots, \phi_n)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder\end{equation*}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederwhere $\hearts$ is an $n$-ary operator in $\Lambda$. Examples are

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder$\Lambda=\{L_p\mid p\in[0,1]\cap\mathbb{Q}\}$, the unary operators

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder$L_p$ of probabilistic modal logic read `with probability at least

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder$p$'; $\Lambda=\{\gldiamond{k}\mid k\in\Nat\}$, the operators

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder$\gldiamond{k}$ of graded modal logic read `in more than $k$

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedersuccessors'; $\Lambda=\{[C]\mid C\subseteq N\}$, the operators $[C]$

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederof coalition logic read `coalition $C$ (a subset of the set $N$ of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederagents) can jointly enforce that'; and, for our main example here,

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder$\Lambda=\{\Rightarrow\}$, the \emph{binary} modal operator

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder$\Rightarrow$ of conditional logic read e.g.\ `if \dots then normally

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder\dots'.

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederCoalgebraic modal logic was originally limited to so-called

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder\emph{rank-$1$ logics} axiomatised by formulas with nesting depth of

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maedermodal operators uniformly equal to $1$~\cite{Schroder05}. It has since

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederbeen extended to the more general non-iterative

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederlogics~\cite{SchroderPattinson08d} and to some degree to iterative

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederlogics, axiomatised by formulas with nested

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedermodalities~\cite{SchroderPattinson08PHQ}. The examples considered here

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederall happen to be rank-$1$, so we focus on this case. In the rank-$1$

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedersetting, it has been shown~\cite{Schroder05} that all logics can be

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederaxiomatised by \emph{one-step rules} $\phi/\psi$, where $\phi$ is

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederpurely propositional and $\psi$ is a clause over formulas of the form

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder$\hearts(a_1,\dots,a_n)$, where the $a_i$ are propositional

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedervariables. In the context of a sequent calculus, this takes the

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederfollowing form~\cite{PattinsonSchroder08b}.

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder\begin{definition}

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder If $S$ is a set (of formulas or variables) then $\Lambda(S)$ denotes

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder the set $\lbrace \hearts(s_1, \dots, s_n) \mid \hearts \in \Lambda

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder \mbox{ is $n$-ary, } s_1, \dots, s_n \in S \rbrace$ of formulas

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder comprising exactly one application of a modality to elements of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder $S$. An \emph{$S$-sequent}, or just a \emph{sequent} in case

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder that $S$ is the set of all formulas, is a finite subset of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder $S \cup \lbrace \neg A \mid A

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder \in S \rbrace$. Then, a \emph{one-step rule}

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder $\Gamma_1,\dots,\Gamma_n/\Gamma_0$ over a set $V$ of variables

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder consists of $V$-sequents $\Gamma_1,\dots,\Gamma_n$, the

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder \emph{premises}, and a $\Lambda(S)$-sequent $\Gamma_0$, the

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder \emph{conclusion}. A \emph{goal} is a set of sequents, typically

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder arising as the set of instantiated premises of a rule application.

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder\end{definition}

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder\noindent A given set of one-step rules then induces an instantiation

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederof the \emph{generic sequent calculus}~\cite{PattinsonSchroder08b}

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederwhich is given by a set of rules $\mathcal{R}_{sc}$ consisting of the

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederfinishing and the branching rules $\mathcal{R}^b_{sc}$ (i.e.\ rules

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederwith no premise or more than one premise), the linear rules

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder$\mathcal{R}^l_{sc}$ (i.e.\ rules with exactly one premise) and the

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedermodal rules $\mathcal R^m_{sc}$, i.e.\ the given one-step rules. The

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederfinishing and the branching rules are presented in

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederFigure~\ref{fig:branching} (where $\top=\neg\bot$ and $p$ is an atom),

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederthe linear rules are shown in Figure~\ref{fig:linear}. So far, all

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederthese rules are purely propositional. As an example for a set of modal

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederone-step rules, consider the modal rules $\mathcal R^m_{sc}$ of the

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederstandard modal logic \textbf{K} as given by Figure~\ref{fig:modalK}.

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder\begin{figure}[!h]

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder \begin{center}

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder \begin{tabular}{| c c c |}

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder \hline

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder & & \\[-5pt]

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder (\textsc {$\neg$F}) \inferrule{ }{\Gamma, \neg\bot} &

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (\textsc {Ax}) \inferrule{ }{\Gamma, p, \neg p} &

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (\textsc {$\wedge$}) \inferrule{\Gamma, A \\ \Gamma, B}{\Gamma, A\wedge B} \\[-5pt]

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder & & \\

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \hline

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder \end{tabular}

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder \end{center}

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder \caption{The finishing and the branching sequent rules $\mathcal{R}^b_{sc}$}

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \label{fig:branching}

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder\end{figure}

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder\begin{figure}[!h]

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder \begin{center}

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder \begin{tabular}{| c c |}

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder \hline

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder & \\[-5pt]

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (\textsc {$\neg\neg$})\inferrule{\Gamma, A}{\Gamma, \neg\neg A} &

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (\textsc {$\neg\wedge$}) \inferrule{\Gamma, \neg A, \neg B}{\Gamma, \neg(A\wedge B)} \\[-5pt]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder & \\

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \hline

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \end{tabular}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \end{center}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \caption{The linear sequent rules $\mathcal{R}^l_{sc}$}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \label{fig:linear}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich\end{figure}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu\begin{figure}[!h]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \begin{center}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \begin{tabular}{| c |}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \hline

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \\[-5pt]

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich (\textsc {\textbf{K}})\inferrule{\neg A_1, \ldots , \neg A_n, A_0}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich {\Gamma, \neg \Box A_1,\ldots,\neg \Box A_n, \Box A_0 } \\[-5pt]

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \\

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \hline

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \end{tabular}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \end{center}

da955132262baab309a50fdffe228c9efe68251dCui Jian \caption{The modal rule of \textbf{K}}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich \label{fig:modalK}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich\end{figure}

da955132262baab309a50fdffe228c9efe68251dCui Jian\noindent This calculus has been shown to be complete under suitable

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedercoherence assumptions on the rule set and the coalgebraic semantics,

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederprovided that the set of rules \emph{absorbs cut and contraction} in a

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederprecise sense~\cite{PattinsonSchroder08b}. We say that a formula is

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\emph{provable} if it can be derived in the relevant instance of the

da955132262baab309a50fdffe228c9efe68251dCui Jiansequent calculus; the algorithms presented below are concerned with

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichthe \emph{provability problem}, i.e.\ to decide whether a given

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichsequent is provable. This is made possible by the fact that the

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskicalculus does not include a cut rule, and hence enables automatic

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskiproof search. For rank-1 logics, proof search can be performed in

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski$\mathit{PSPACE}$ under suitable assumptions on the representation of

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichthe rule set~\cite{SchroderPattinson09,PattinsonSchroder08b}. The

53310804002cd9e3c9c5844db3b984abcf001788Christian Maedercorresponding algorithm has been implemented in the system

797595aad6dfd626bc1c9df52616f1ac4235c669Till MossakowskiCoLoSS~\cite{CalinEA09} which remains under continuous

933baca0720dae81434de384b32a93b47e754d09Christian Maederdevelopment. Particular attention is being paid to finding heuristic

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskioptimisations to enable practically efficient proof search, as

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidescribed here.

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichOur running example used in the presentation of our optimisation

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichstrategies below is conditional logic as mentioned above. The most

da955132262baab309a50fdffe228c9efe68251dCui Jianbasic conditional logic is $\textbf{CK}$~\cite{Chellas80} (we shall

da955132262baab309a50fdffe228c9efe68251dCui Jianconsider a slightly extended logic below), which is characterised by

da955132262baab309a50fdffe228c9efe68251dCui Jianassuming normality of the right-hand argument of the non-monotonic

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichconditional $\Rightarrow$, but only replacement of equivalents in the

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichleft-hand arguments. Absorption of cut and contraction requires a

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichunified rule set consisting of the rules depicted in Fig.~\ref{fig:modalCK}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichwith $A=C$ abbreviating the pair of sequents $\neg A,C$ and $\neg

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichC,A$.

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich\begin{figure}[!h]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \begin{center}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \begin{tabular}{| c |}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \hline

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \\[-5pt]

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu (\textsc {\textbf{CK}})\inferrule{A_0=A_1;\dots;A_n=A_0\\ \neg B_1,\dots,\neg B_n,B_0}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski {\Gamma, \neg(A_1\Rightarrow B_1),\dots,\neg(A_n\Rightarrow B_n),(A_0\Rightarrow B_0)}\\[-5pt]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \\

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \hline

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \end{tabular}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \end{center}

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \caption{The modal rule of \textbf{CK}}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski \label{fig:modalCK}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich\end{figure}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich%\begin{equation*}

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich% \infrule{A_0=A_1;\;\dots;\; A_n=A_0\quad \neg B_1,\dots,\neg B_1,B_0}

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder% {\neg(A_1\Rightarrow B_1),\dots,\neg(A_n\Rightarrow B_n),(A_0\Rightarrow B_0)}

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder%\end{equation*}

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian MaederThis illustrates two important points that play a role in the

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichoptimisation strategies described below. First, the rule has a large

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederbranching degree both existentially and universally -- we have to

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maedercheck that there \emph{exists} a rule proving some sequent such that

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder\emph{all} its premises are provable, and hence we have to guess one

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederof exponentially many subsequents to match the rule and then attempt

da955132262baab309a50fdffe228c9efe68251dCui Jianto prove linearly many premises; compare this to linearly many rules

da955132262baab309a50fdffe228c9efe68251dCui Jianand a constant number of premises per rule (namely, $1$) in the case

da955132262baab309a50fdffe228c9efe68251dCui Jianof $\textbf{K}$ shown above. Secondly, many of the premises are short

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichsequents. This will be exploited in our memoisation strategy. We note

da955132262baab309a50fdffe228c9efe68251dCui Jianthat \emph{labelled} sequent calculi for conditional logics have been

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescudesigned previously~\cite{OlivettiEA07} and have been implemented in

f2c050360525df494e6115073b0edc4c443a847cMihai Codescuthe CondLean prover~\cite{OlivettiPozzato03}; contrastingly, our

f2c050360525df494e6115073b0edc4c443a847cMihai Codescucalculus is unlabelled, and turns out to be conceptually simpler. The

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maedercomparison of the relative efficiency of labelled and unlabelled

da955132262baab309a50fdffe228c9efe68251dCui Jiancalculi remains an open issue for the time being.

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder\section{The Algorithm}

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaederAccording to the framework introduced above, we now devise a generic

53310804002cd9e3c9c5844db3b984abcf001788Christian Maederalgorithm to decide the provability of formulas, which is easily

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maederinstantiated to a specific logic by just implementing the relevant modal

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskirules.

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiAlgorithm~\ref{alg:seq} makes use of the sequent rules in the

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskifollowing manner: In order to show the \emph{provability} of a formula

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder$\phi$, the algorithm starts with the sequent $\{\phi\}$ and just

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskikeeps trying to apply all of the sequent rules in $\mathcal{R}_{sc}$ to it,

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maedergiving precedence to the linear rules. Below, we refer to a sequent

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederas \emph{open} if it has not yet been checked for provability. Under

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskisuitable tractability assumptions on the rule set as

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiin~\cite{SchroderPattinson09,PattinsonSchroder08b}, this algorithm

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederrealises the theoretical upper bound $\mathit{PSPACE}$. It is the

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskistarting point of the proof search algorithms employed in CoLoSS,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskibeing essentially a sequent reformulation of the algorithm described

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiin~\cite{CalinEA09}, where it is easily verified that correctness and termination

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederof the algorithm are preserved by this reformulation; optimisations of this

53310804002cd9e3c9c5844db3b984abcf001788Christian Maederalgorithm are the subject of the present work.

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder%\begin{algorithm}[h]

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski%\fbox{\parbox{\myboxwidth}{

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder\begin{alg}(Decide provability of a sequent $\Gamma$)

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski\begin{upshape}

bba825b39570777866d560bfde3807731131097eKlaus Luettich \begin{algenumerate}

da955132262baab309a50fdffe228c9efe68251dCui Jian \item Try all possible applications of rules from $\mathcal{R}_{sc}$ to $\Gamma$,

da955132262baab309a50fdffe228c9efe68251dCui Jian giving precedence to linear rules. For every such rule application,

bba825b39570777866d560bfde3807731131097eKlaus Luettich perform the following steps, and answer `provable' in case these steps

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder succeed for one of the rule applications.

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \item Let $\Lambda$ denote the set of premises arising from the rule

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski application.

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \item Check recursively that every sequent in $\Lambda$ is provable.

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \end{algenumerate}

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder\end{upshape}

c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder\label{alg:seq}

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder\end{alg}

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder%}}

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder%\end{algorithm}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder%\begin{proposition}

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder%\begin{upshape}

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder%Let $\mathcal{R}_{sc}$ be strictly one-step complete, closed under contraction,

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder%and PSPACE-tractable. Then Algorithm~\ref{alg:seq} is sound and complete w.r.t. provability

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder%and it is in PSPACE.

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder%\end{upshape}

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder%\end{proposition}%

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder%\begin{proof}

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder%We just note, that Algorithm~\ref{alg:seq} is an equivalent implementation of the algorithm proposed

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski%in~\cite{SchroderPattinson09}. For more details, refer to ~\cite{SchroderPattinson09}, Theorem 6.13.

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder%\end{proof}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder\subsection{The conditional logic instance}

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder

0647a6c86b231e391826c7715338ba29cb4934c0Christian MaederThe genericity of the introduced sequent calculus allows us to easiliy

53310804002cd9e3c9c5844db3b984abcf001788Christian Maedercreate instantiations of Algorithm~\ref{alg:seq} for a large variety

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maederof modal logics:

63324a97283728a30932828a612c7b0b0f687624Christian Maeder

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder\noindent For instance it has been shown in~\cite{PattinsonSchroder09a} that the

63324a97283728a30932828a612c7b0b0f687624Christian Maedercomplexity of \textbf{CKCEM} is $\mathit{coNP}$, using a dynamic

63324a97283728a30932828a612c7b0b0f687624Christian Maederprogramming approach in the spirit of~\cite{Vardi89}; in fact, this

63324a97283728a30932828a612c7b0b0f687624Christian Maederwas the original motivation for exploring the optimisation strategies

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maederpursued here.

a975722baf6fee1ca3e67df170c732c4abd0a945Christian MaederDue to this reason, we restrict ourselves to the examplary

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maederconditional logic \textbf{CKCEM} for the remainder of this section;

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maederslightly adapted versions of the optimisation will work for other

63324a97283728a30932828a612c7b0b0f687624Christian Maederconditional logics. \textbf{CKCEM} is characterised by the additional

63324a97283728a30932828a612c7b0b0f687624Christian Maederaxioms of \emph{conditional excluded middle} $(A\Rightarrow

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederB)\lor(A\Rightarrow\neg B)$, which to absorb cut and contraction is

933baca0720dae81434de384b32a93b47e754d09Christian Maederintegrated in the rule for \textbf{CK} as shown in Figure~\ref{fig:modalCKCEM}.

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jian%By setting $\mathcal R^m_{sc}$ for to the

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu%rule shown in Figure~\ref{fig:modalCKCEM},

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu% (where $A_a = A_b$ is

da955132262baab309a50fdffe228c9efe68251dCui Jian%shorthand for $A_a\rightarrow A_b\wedge A_b\rightarrow A_a$),

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu%we obtain an algorithm for deciding provability (and satisfiability)

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu%of conditional logic.

da955132262baab309a50fdffe228c9efe68251dCui Jian

da955132262baab309a50fdffe228c9efe68251dCui Jian\begin{figure}[h!]

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder \begin{center}

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder \begin{tabular}{| c |}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \hline

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \\[-5pt]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (\textsc {\textbf{CKCEM}})\inferrule{A_0 = A_1;\ldots;A_n = A_0 \\ B_0,\ldots, B_j,\neg B_{j+1},\ldots,\neg B_n}

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

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

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \\

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \hline

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \end{tabular}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \end{center}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \caption{The modal rule $\textbf{CKCEM}$ of conditional logic}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder \label{fig:modalCKCEM}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\end{figure}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederIn the following, we use the notions of \emph{conditional antecedent} and

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\emph{conditional consequent} to refer to the parameters of the modal operator of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederconditional logic.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederIn order to decide using Algorithm~\ref{alg:seq} whether there is an

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance of the modal rule of conditional logic which can be applied

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederto the actual current sequent, it is necessary to create a preliminary

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederpremise for each possible combination of equalities of all the

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederpremises of the modal operators in this sequent. This results in

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder$2^n-1$ new premises for a sequent with $n$ top-level modal

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederoperators.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\begin{example}\label{ex:cond}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederFor the sequent $\Gamma=\{(A_0\Rightarrow B_0),

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder(A_1\Rightarrow B_1), (A_2\Rightarrow B_2)\}$, there are $2^3=8$

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederpossible instances of the rule to be tried, corresponding to the

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedernon-empty subsequents of the goal; the premise to be checked for

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder$I\subseteq\{1,2,3\}$ consists of $A_i=A_j$ for $i,j\in I$, and

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder$\{B_i\mid i\in I\}$.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\end{example}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\noindent It seems to be a more intelligent approach to first

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederpartition the set of all antecedents of the top-level modal operators

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederin the current sequent into equivalence classes with respect to

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederlogical equality. This partition allows for a significant reduction

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederboth of the number of rules to be tried and of the number of premises

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederto be actually proved for each rule.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\begin{example}

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

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederknowledge that $A_0=A_1$, $A_1\neq A_2$ and $A_0\neq A_2$, it is immediate

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederthat there are just two reasonable instations of the modal rule, leading

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederto the two premises $\{\{B_0,B_1\}\}$ and $\{\{B_2\}\}$. For the

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederfirst of these two premises, note that it is not necessary to show the

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederequivalence of $A_0$ and $A_1$ again.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\end{example}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\noindent In the case of conditional logic, observe the following:

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederSince the modal antecedents that appear in a formula are not being

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederchanged by any rule of the sequent calculus, it is possible to extract

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederall possibly relevant antecedents of a formula even \emph{before} the

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederactual sequent calculus is applied. This allows us to first compute

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederthe equivalence classes of all the relevant antecedents and then feed

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederthis knowledge into the actual sequent calculus, as illustrated next.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\section{The Optimisation}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\begin{definition}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederA conditional antecedent of \emph{modal nesting depth} $i$ is a

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederconditional antecedent which contains at least one antecedent of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedermodal nesting depth $i-1$ and which contains no antecedent

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederof modal nesting depth greater than $i-1$. A

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederconditional antecedent of nesting depth 0 is an antecedent

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederthat does not contain any further modal operators.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederLet $a_i$ denote the set of all conditional antecedents of modal

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedernesting depth $i$. Further, let $\prems(n)$ denote the set of all

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederconditional antecedents of modal nesting depth at most $n$ (i.e.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder$\prems(n)=\bigcup_{j=1..n}^{} a_j$).

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederFinally, let $depth(\phi)$ denote the maximal modal nesting in

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederthe formula $\phi$.

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder\end{definition}

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder%\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 sequents together with a function

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

a \emph{knowledge base}.

\end{definition}

\noindent We may now construct an optimized algorithm which allows us

to decide provability (and satisfiability) of formulas more

efficiently in some cases. The optimized algorithm is constructed from

two functions (namely from the actual proving function and from the

so-called \emph{pre-proving} function):

%\begin{algorithm}[h]

\begin{alg}\label{alg:opt}

(Decide provability of $\phi$ using the knowledge

base $(\mathcal{K},\eval)$)

{\upshape

\begin{algenumerate}

\item\label{step:look-up} If $\Gamma\in\mathcal{K}$, answer `provable' if

$\eval(\Gamma)=\top$, else `unprovable'. Otherwise:

\item\label{step:rule} Try all possible applications of rules from

$\mathcal{RO}_{sc}$ to $\Gamma$, giving precedence to linear rules,

where $\mathcal{RO}_{sc}$ is an optimised set of rules taking into

account the knowledge base, as explained below. For every such rule

application, perform the following steps, and answer `provable' in

case these steps succeed for one of the rule applications.

\item Let $\Lambda$ denote the set of premises arising from the rule

application.

\item Check recursively that every sequent in $\Lambda$ is provable.

\end{algenumerate}

}

\label{alg:optSeq}

\end{alg}

%\end{algorithm}

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

Algorithm~\ref{alg:seq} but relies on the knowledge base passed to it

and moreover uses a modified set of rules $\mathcal{RO}_{sc}$. The set

of rules $\mathcal{RO}_{sc}$ makes appropriate use of the knowledge

base. It 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}. The point is that the premises

$A_0=\dots=A_n$ are replaced by side conditions representing lookup in

the knowledge base. This improves on standard memoising as embodied by

the lookup operation in step~\ref{step:look-up} of the above algorithm

in that existential branching over potentially applicable rules is

reduced: the rule does not even match the target sequent unless the

equivalence premises are already in the knowledge base. This is still

a complete system due to the way memoising is organised, as explained

below.

\begin{figure}[h!]

\begin{center}

\begin{tabular}{| c |}

\hline

\\[-5pt]

(\textsc {\textbf{CKCEM}$^m$})\inferrule{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]

\\

\hfill ($\bigwedge{}_{i,j\in\{1..n\}}{\eval(A_i=A_j)=\top}$)\\

\hline

\end{tabular}

\end{center}

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

\label{fig:modalCKCEMm}

\end{figure}

%\begin{algorithm}[h]

\noindent The knowledge base used in Algorithm~\ref{alg:opt} is

computed in Algorithm~\ref{alg:preprove}. The algorithm proceeds by

dynamic programming with stages corresponding to modal nesting depth,

in the spirit of~\cite{Vardi89}. Thus, in order to show the

equivalence of two conditional antecedents of nesting depth at most

$i$, we assume that the equivalences $\mathcal{K}_{i}$ between modal

antecedents of nesting depth less than $i$ have already 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 base $(\mathcal{K}_{i},\eval_i)$.

\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

formulas $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 `provable'

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

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

value as result.

\label{alg:preprove}

\end{upshape}

\end{alg}

%\end{algorithm}

\subsection{Treatment of Requisite Equivalences Only}

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

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

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

\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 will not be needed

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

\label{ex:requis}

\end{example}

Based on this observation it is possible to define a set $C$ of classes

of so-called \emph{connected} subformulas of a given formula $\phi$. We require that

each class $c_i\in C$ contains only formulas that are pairwise connected in $\phi$. Given

a formula $\phi$, two subformulas of it are said to be connected in $\phi$ if they \emph{may}

both appear in the conclusion of the application of a modal rule during the course of a proof

of $\phi$. Two subformulas of $\phi$ are said to be \emph{independent} in $\phi$ if they are

not connected.

In the case of conditional logic with conditional excluded middle, two formulas are connected

if they appear at identical positions (modulo different choice of modal operator on each level)

within $\phi$. We use the notions of \emph{classes of connected antecedents} (and \emph{classes of

connected consequents}) to refer to the set of those classes which only contain antecedents (and consequents,

respectively).

\begin{example}

Considering again the formula from Example~\ref{ex:requis}, $\phi$ has the following classes

of connected antecedents:

\begin{quote}

$c_1=\{((p_0\Rightarrow p_1)\Rightarrow p_2, (p_5\Rightarrow p_6)\Rightarrow p_7)\}$,

$c_2=\{(p_0\Rightarrow p_1, p_5\Rightarrow p_6)\}$ and $c_3=\{(p_0,p_5)\}$.

\end{quote}

The classes of connected consequents in $\phi$ are as follows:

\begin{quote}

$c_4=\{(p_4, p_8)\}$, $c_5=\{p_2, p_7)\}$ and $c_6=\{p_1, p_6)\}$.

\end{quote}

\end{example}

Since two independent conditional 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 conditional antecedents. It is then obvious that

any possibly requisite 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 are in fact not needed

(since antecedents may indeed be connected and still it is possible that they never appear together in an application

of the modal rule - this is the case whenever two preceding antecedents are not logically equivalent).

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

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

that before proving any equivalences, Algorithm~\ref{alg:optPreprove} partitions the

set of all relevant modal antecedents into the set of classes of connected antecedents.

Then the algorithm treats equivalences between any two pairs in each of the classes.

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 $C_i$ of all \emph{classes of connected} 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: For each $c_i\in C_i$, let $eq_{c_i}$ denote the set of all equalities $A_a = A_b$ for different

pairs of formulas $A_a,A_b\in c_i$. For each $eq_{c_i}$, compute

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

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

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

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

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

return value as result.

\label{alg:optPreprove}

\end{upshape}

\end{alg}

%\end{algorithm}

\section{Implementation}

The proposed optimized algorithms have been implemented (using the programming

language Haskell) as part of the generic coalgebraic modal logic satisfiability

solver (\COLOSS\footnote{As already mentioned above, more information about \COLOSS,

a web-interface to the tool and

the tested benchmarking formulas can be found at \url{http://www.informatik.uni-bremen.de/cofi/CoLoSS/}}).

\COLOSS~provides the general coalgebraic framework in which the 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 matching function for conditional logic in \COLOSS~was hence adapted in order to realize

the different optimisations (closely following Algorithms~\ref{alg:seq},~\ref{alg:preprove} and

~\ref{alg:optPreprove}), so that \COLOSS~now provides an efficient algorithm for

deciding the provability (and satisfiability) of conditional logic formulas.

\subsection{Comparing the Proposed Algorithms}

\label{sec:bench}

In order to show the relevance of the proposed optimisations, we devise several classes

of conditional formulas. Each class has a characteristic general shape, defining its

complexity w.r.t. different parts of the algorithms and thus exhibiting specific

advantages or disadvantages of each algorithm:

\begin{itemize}

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

inequivalent atoms and $2^i-1$ independent 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}

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

a formula contains many modal antecedents which appear at different depths. A comparison of the different

algorithms w.r.t. formulas \verb|bloat(|$i$\verb|)| is depicted in Figure~\ref{fig:benchBloat}.

Since Algorithm~\ref{alg:preprove} does not check whether pairs of modal antecedents are independent or connected,

it performs considerably worse than Algorithm~\ref{alg:optPreprove} which only attempts to prove the logical

equivalence of formulas which are not independent. Algorithm~\ref{alg:seq} has the best performance in this

extreme case, as it only has to consider pairs of modal antecedents which actually appear during the course

of a proof. This is the price to pay for the optimisation by dynamic programming.

\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.007s & 0.007s & 0.007s\\

2 & 0.007s & 0.007s & 0.007s\\

3 & 0.007s & 0.008s & 0.008s\\

4 & 0.008s & 0.017s & 0.012s\\

5 & 0.009s & 0.112s & 0.048s\\

6 & 0.010s & 1.154s & 0.416s\\

7 & 0.012s & 11.998s & 4.116s\\

\hline

\end{tabular}

\end{center}

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

\label{fig:benchBloat}

\end{figure}

\begin{itemize}

\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 consists of formulas which contain logically (but not sytactically) equivalent antecedents.

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

of the considered formula. A comparison of the different algorithms w.r.t. formulas \verb|conjunct(|$i$\verb|)| is depicted in

Figure~\ref{fig:benchConjunct}. It is obvious that the optimized algorithms perform considerably better than the unoptimized

Algorithm~\ref{alg:seq}. The reason for this is that Algorithm~\ref{alg:seq} repeatedly proves equivalences between the same

pairs of modal antecedents. The optimized algorithms on the other hand are equipped with knowledge about the modal antecedents,

so that these equivalences have to be proved only once. However, even the runtime of the optimized algorithms is exponential in $i$,

due to the exponentially increasing complexity of the underlying propositional formula. Note that the use of propositional tautologies (such as

$A \leftrightarrow (A\wedge A) $ in this case) would help to greatly reduce the computing time for \verb|conjunct(|$i$\verb|)|.

Optimisation of propositional reasoning is not the scope of this paper though, thus we devise the following examplary class of formulas

(for which propositional tautologies would not help):

\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.008s & 0.008s\\

2 & 0.009s & 0.009s & 0.009s\\

3 & 0.011s & 0.010s & 0.010s\\

4 & 0.058s & 0.011s & 0.011s\\

5 & 1.335s & 0.014s & 0.015s\\

6 & 42.885s & 0.038s & 0.040s\\

7 & $>$600.000s & 0.220s & 0.232s\\

8 & $\gg$600.000s & 1.944s & 2.019s\\

9 & $\gg$600.000s & 17.826s & 18.790s\\

\hline

\end{tabular}

\end{center}

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

\label{fig:benchConjunct}

\end{figure}

\begin{itemize}

\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\ldots\wedge p_{(j+(i-1)) \bmod i}$

\end{quote}

This class contains complex formulas for which the unoptimized

algorithm should not be efficient any more: Only the combined

knowledge about all appearing modal antecedents $A^i_j$ allows the

proving algorithm to reach all modal consequents $c_n$, and only the

combined sequent $\{(c_1\wedge\ldots\wedge c_i),\neg c_1,\ldots,\neg

c_i\}$ (containing every appearing consequent) is provable. For

formulas from this class (specifically designed to show the advantages

of optimization by dynamic programming), the optimized algorithms

vastly outperform the unoptimized algorithm (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.007s & 0.007s & 0.007s\\

2 & 0.007s & 0.007s & 0.007s\\

3 & 0.009s & 0.009s & 0.009s\\

4 & 0.017s & 0.010s & 0.010s\\

5 & 0.133s & 0.012s & 0.012s\\

6 & 0.305s & 0.015s & 0.016s\\

7 & 430.684s& 0.018s & 0.022s\\

8 & $\gg$600.000s& 0.023s & 0.029s\\

9 & $\gg$600.000s& 0.029s & 0.044s\\

\hline

\end{tabular}

\end{center}

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

\label{fig:benchExplode}

\end{figure}

The tests were conducted on a Linux PC (Dual Core AMD Opteron 2220S

(2800MHZ), 16GB RAM). It is obvious that a significant increase of

performance may be obtained through the proposed optimisations. In

general, the performance of the implementation of the proposed

algorithms in the generic reasoner CoLoSS is comparable to dedicated

conditional logic provers such as CondLean; a direct comparison is

presently made difficult by the fact that the benchmarking formulas

used to evaluate CondLean are not listed explicitly

in~\cite{OlivettiPozzato03}.

\section{Generalized Optimisation}

As previously mentioned, the demonstrated optimisation 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 optimisation 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 optimisation may be applied}

\label{fig:modalOpt}

\end{figure}

Then we 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 of form $S_i$ (where $S_i$ is a sequent

from the premise of rule (\textbf{Opt})) over at most two formulas

$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

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

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

as result.

\end{upshape}

\label{alg:genOptPreprove}

\end{alg}

\end{algorithm}

This new Algorithm~\ref{alg:genOptPreprove} may then be used to decide provability of formulas,

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]

\hspace{75pt}(\textsc {\textbf{Opt}$^m$}) \inferrule{ \mathcal{S} }

{ \Gamma }\hspace{75pt}\vspace{3pt}\\[-5pt]

\hfill ($\bigwedge{}_{i\in\{1..n\}}{\eval(S_i)=\top}$) \\

\hline

\end{tabular}

\end{center}

\caption{The general optimized rule}

\label{fig:modModalOpt}

\end{figure}

\begin{example}

The following two cases are instances of the generic optimisation:

\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{ {} }

{ \Box A = \Box B }

\end{center}

\end{quote}

with the side-condition $\eval(A=B)=\top$.

\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{ {} }

{ \Box A \rightarrow \Box B }

\end{center}

\end{quote}

with the side-condition $\eval(A\rightarrow B)=\top$.

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 optimisation 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{Conclusion}

We presented (from a practical point of view) two optimisations for reasoning

in conditional logic:

\begin{itemize}

\item The first optimisation makes use of the concept of dynamic programming

in order to separate the two tasks that showing validity of formulas in conditional

logic consists of: The first task of proving equivalences of antecedents and the second task

of ordinary sequent proving. The use of dynamic programming substantially decreases the

branching breadth of the resulting sequent calculus.

\item The second proposed optimisation introduces a strategy to reduce the amount

of pairs of antecedents whose equivalence has to be considered. This is achieved

by distinguishing between connected and independent pairs of modal arguments.

\end{itemize}

When both optimisations are applied at the same time, a significant increase in

performance of the sequent algorithm for conditional logic can be observed.

This was shown in

Section~\ref{sec:bench} by considering the results of benchmarking a Haskell

implementation (which forms part of the generic proving tool \COLOSS) of the

optimised algorithms.

It remains as an open question whether the gain in perfomance which is obtained

by optimising the algorithm for conditional logic may be transferred to other

logics by making use of the generic optimisation strategy as described in the

last section.

\bibliographystyle{myabbrv}

\bibliography{coalgml}

\end{document}