Commit 9646cea8 authored by ehilin02's avatar ehilin02
Browse files

coNP upper bound

parent 5749735d
......@@ -49,18 +49,30 @@ In Section~\ref{ssec:ent-1}, we consider the special case
The general case is dealt with in Section~\ref{ssec:ent-all};
the procedure calls the special case for the first atom of the consequent with
all the compatible prefixes of the antecedent, and
it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. We derive the coNP upper bound from the aforementioned decision procedure as follows:
it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones.
We show how to derive the coNP upper bound from the aforementioned decision procedure. We first observe the following facts.
\begin{enumerate}
\item The entailment problem is reduced to at most exponentially many
\emph{ordered entailment problems} since there are exponentially many total preorders.
\item Each ordered entailment problem can be reduced further to exponentially many \emph{special ordered entailment problems} where there is one spatial atom in the consequent.
\item The original entailment problem is invalid iff there is an invalid special ordered entailment problem instance.
\item The original entailment problem is valid iff all of at most exponentially many
\emph{ordered entailment problems} are valid, since there are exponentially many total preorders.
\item For each ordered entailment problem, it is valid iff all of at most exponentially many \emph{special ordered entailment problems}, where the consequent contains only one spatial atom, are valid.
%\item The original entailment problem is invalid iff there is an invalid special ordered entailment problem instance.
\item The special ordered entailment problem is in coNP.
\end{enumerate}
Therefore, to show that $\varphi \models \psi$ is not valid, we
\begin{itemize}
\item first guess a total preorder and obtain an ordered entailment problem,
\item then guess for the ordered entailment problem one special ordered entailment problem where the consequent contains only one spatial atom,
\item and finally guess and verify in polynomial time a polynomial-size witness for the invalidity of the special ordered entailment problem.
\end{itemize}
The above procedure runs in nondeterministic polynomial time, thus showing the invalidity of the entailment problem is in NP. From this, we conclude that the entailment problem of {\slah} is in coNP.
%At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable,
%then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$,
%the the entailment $\varphi \models \psi$ does not hold.
\smallskip
In the sequel, we assume that $\abs(\varphi)$ is satisfiable and $\abs(\varphi) \models \abs(\psi)$. Otherwise, the entailment is trivially invalid.
\subsection{Decomposition into ordered entailments}
......
......@@ -36,9 +36,9 @@
\newcommand{\EPbA}{\textsf{EPA}}
\newcommand{\qfpa}{\textsf{QFPA}}
\newcommand{\sphead}{\texttt{head}}
\newcommand{\sphead}{\texttt{start}}
\newcommand{\sptail}{\texttt{tail}}
\newcommand{\sptail}{\texttt{end}}
% ---- Syntax ----
......@@ -102,8 +102,8 @@
\newcommand \satoms {{\tt Atoms}}
\newcommand \patoms {{\tt PAtoms}}
\newcommand \atoms {{\tt Atoms}}
\newcommand \atomhead {{\tt head}}
\newcommand \atomtail {{\tt next}}
\newcommand \atomhead {{\tt start}}
\newcommand \atomtail {{\tt end}}
\newcommand \vars {{\tt Vars}}
\newcommand{\addr}{\mathcal{A}}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment