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.