Let $T$ be a theory that only contains renamable horn formulas. What is the complexity of deciding if the closed world assumption $CWA(T)$ is consistent?
The closed world assumption is defined as follows:
$CWA(T):=T\cup \{\neg p : p\text{ is atom } T \not\models p\}$
Renamable horn formulas are CNF formulas that can be renamed to horn formulas by negating a variable in the formula for example
$(x_1\vee x_2 \vee x_3)\wedge (\neg x_3 \vee\neg x_4)$
is not a horn formula but can be renamed by the renaming $R=\{x_2,x_3\}$ to get the equally satisfiable formula
$(x_1\vee \neg x_2 \vee \neg x_3)\wedge (x_3 \vee\neg x_4)$
My findings so far:
We call a theory $\Phi$ of first order logic inconsistent if $\exists \phi \in \Phi$ such that $\Phi\models \phi$ and $\Phi\not\models \phi$. Otherwise $\Phi$ is consistent.
To check whether $CWA(T)$ is consistent it is sufficient to check if $\Phi=\bigwedge_{\phi\in CWA(T)}\phi$ is satisfiable.
Algorithm to construct CWA:
To compute $CWA(T)$ we need to know if $T\models x_i$ for all variables in $T$. This can be done by considering $\Psi=\bigwedge_{\psi\in T}\psi$ and then checking if $\Psi \rightarrow x_i$ or equivalently $\neg x_i \rightarrow \neg\Psi$. Therefore if we set $x_i=0$ in $\Psi$ and $\Psi$ is not satisfiable it follows $T\models x_i$, otherwise $T\not\models x_i$.
First create an set $I=\{\emptyset\}$
For all variables defined by the index $i=0,...,n$ we do the following calculation:
1.] set $x_i=0$ in $\Psi=\bigwedge_{\psi\in T}\psi$
2.] if $\Psi$ is not satisfiable $I=I\cup\{x_i\}$
By considering the elements of $I$ we can conclude $CWA(T)=T\cup\{\neg x_i:x_i\not\in I\}$.
Deciding if CWA(T) is consistent is at least NP-hard:
let $C_1,...,C_m$ be clauses of an arbitrary 3-SAT instance and $C_{m+1}=(u\vee v)$ such that $u,v$ are fresh atoms. Then $T=\{C_1,...,C_m,C_{m+1}\}$ contains only renamable Horn clauses.
To decide if $CWA(T)$ is consistent we need to decide if $u$ is free for negation. This follows by checking if $T\models u$. Therefore we assume $u=0$ and check if $C_1\wedge C_2 \wedge ... \wedge v$ is not satisfiable. Since v occurs in no other clause, the formula is not satisfiable if $C_1\wedge ... \wedge C_m$ is not satisfiable, but $C_1\wedge ... \wedge C_m$ is an arbitrary 3-SAT instance and so checking if $CWA(T)$ is consistent is at least NP-hard.
