# About the complexity of deciding if the closed world assumption for renamable Horn CNF is consistent

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.