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.

  • $\begingroup$ May I ask what larger goal you are trying to reach by solving this problem? $\endgroup$ – ShyPerson Aug 20 '20 at 5:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.