Closed World Assumption - Formalization in Logic

Formalization in Logic

The first formalization of the closed world assumption in formal logic consists in adding to the knowledge base the negation of the literals that are not currently entailed by it. The result of this addition is always consistent if the knowledge base is in Horn form, but is not guaranteed to be consistent otherwise. For example, the knowledge base

entails neither nor .

Adding the negation of these two literals to the knowledge base leads to

which is inconsistent. In other words, this formalization of the closed world assumption sometimes turns a consistent knowledge base into an inconsistent one. The closed world assumption does not introduce an inconsistency on a knowledge base exactly when the intersection of all Herbrand models of is also a model of ; in the propositional case, this condition is equivalent to having a single minimal model, where a model is minimal if no other models has a subset of variables assigned to true.

Alternative formalizations not suffering from this problem have been proposed. In the following description, the considered knowledge base is assumed to be propositional. In all cases, the formalization of the closed world assumption is based on adding to the negation of the formulae that are “free for negation” for, i.e., the formulae that can be assumed to be false. In other words, the closed world assumption applied to a propositional formula generates the formula:

.

The set of formulae that are free for negation in can be defined in different ways, leading to different formalizations of the closed world assumption. The following are the definitions of being free for negation in the various formalizations.

CWA (closed world assumption)

is a positive literal not entailed by ;

GCWA (generalized CWA)

is a positive literal such that, for every positive clause such that, it holds ;

EGCWA (extended GCWA)

same as above, but is a conjunction of positive literals;

CCWA (careful CWA)

same as GCWA, but a positive clause is only considered if it is composed of positive literals of a given set and (both positive and negative) literals from another set;

ECWA (extended CWA)

similar to CCWA, but is an arbitrary formula not containing literals from a given set.

The ECWA and the formalism of circumscription coincide on propositional theories. The complexity of query answering (checking whether a formula is entailed by another one under the closed world assumption) is typically in the second level of the polynomial hierarchy for general formulae, and ranges from P to coNP for Horn formulae. Checking whether the original closed world assumption introduces an inconsistency requires at most a logarithmic number of calls to an NP oracle; however, the exact complexity of this problem is not currently known.