\documentclass[11pt,final,notitlepage,onecolumn]{article}%
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{amsmath}
\usepackage{amssymb}%
\date{}
\oddsidemargin 0in \evensidemargin 0in \textwidth 6.5in \topmargin 0in \textheight 8.5in
\begin{document}
% PSPACE Bounds for Rank-1 Modal Logics 
{\bf Algorithm for deciding SAT of $\phi\in\mathcal{F}(\Lambda)$}
\begin{itemize}
\item (1) (Existential) Guess a propositionally consistent pseudovaluation $H$ for $\phi$.
\item (2) (Universal) Choose a contracted clause $\rho\neq\bot$ over $MA(H)$ such that $H\vdash_{PL}\neg\rho$.
\item (3) (Universal) Choose an $\mathcal{R}_C$-matching $[R]$ of $\rho$.
\item (4) (Existential) Guess a clause $\gamma$ from the CNF of the premise of $R$.
\item (5) Recursively check that $\neg\gamma\sigma(R,\rho)$ is satisfiable.
\end{itemize}
The algorithm succeeds if all possible choices at steps marked universal lead to successful termination, and for all steps marked existential, there exists a choice leading to successful termination. Concerning the first step, note that the only way for a pseudovaluation to be propositionally inconsistent is to contain both $L\rho$ and $\neg L\rho$ for some modal atom $L\rho$.

\bigskip

% Detailed Interpretation
{\bf Interpretation for our Haskell Implementation}
\begin{itemize}
\item (1) When getting to this step it is supposed that $\phi$ is our predefined formula type. We then extract all top-layer modal atoms of the given formula (will be stored in a list) and generate all combinations of possible instantiations of these modal atoms (thus getting a list of propositional formulas). Filter the latter so we keep only the ones evaluating to true.
\item (2) Generate all nonempty clauses $\rho$ (as a list) for the kept pseudovaluations above such that the formula instantiated with the particular pseudovaluation entails $\neg\rho$. These clauses will be stored in a list (one list of $\rho$'s for each good pseudovaluation).
\item (3) Test each of the $\rho$'s against the predefined rules of the top-layer logic and for each $\rho$ return a list containing the "numeric" order of the atoms in the matched rule.
\item (4) For each $\rho$ and matching rule (stored as in the previous step) generate a list with all clauses from the CNF of the premise of the rule.
\item (5) For each clause $\gamma$ of the list obtained above check the satisfiability of $\neg\gamma\sigma(R,\rho)$ and recurse by removing the modal "layers" as in the first 4 steps.
\end{itemize}

\bigskip
\end{document}
