Closed-world assumption

Last updated

The closed-world assumption (CWA), in a formal system of logic used for knowledge representation, is the presumption that a statement that is true is also known to be true. Therefore, conversely, what is not currently known to be true, is false. The same name also refers to a logical formalization of this assumption by Raymond Reiter. [1] The opposite of the closed-world assumption is the open-world assumption (OWA), stating that lack of knowledge does not imply falsity. Decisions on CWA vs. OWA determine the understanding of the actual semantics of a conceptual expression with the same notations of concepts. A successful formalization of natural language semantics usually cannot avoid an explicit revelation of whether the implicit logical backgrounds are based on CWA or OWA.

Contents

Negation as failure is related to the closed-world assumption, as it amounts to believing false every predicate that cannot be proved to be true.

Example

In the context of knowledge management, the closed-world assumption is used in at least two situations: (1) when the knowledge base is known to be complete (e.g., a corporate database containing records for every employee), and (2) when the knowledge base is known to be incomplete but a "best" definite answer must be derived from incomplete information. For example, if a database contains the following table reporting editors who have worked on a given article, a query on the people not having edited the article on Formal Logic is usually expected to return "Sarah Johnson".

Edit
EditorArticle
John DoeFormal Logic
Joshua A. NortonFormal Logic
Sarah JohnsonIntroduction to Spatial Databases
Charles PonziFormal Logic
Emma Lee-ChoonFormal Logic


In the closed-world assumption, the table is assumed to be complete (it lists all editor-article relationships), and Sarah Johnson is the only editor who has not edited the article on Formal Logic. In contrast, with the open-world assumption the table is not assumed to contain all editor-article tuples, and the answer to who has not edited the Formal Logic article is unknown. There is an unknown number of editors not listed in the table, and an unknown number of articles edited by Sarah Johnson that are also not listed in the table.

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 model 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 knowledge base generates the knowledge base

.

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 ; [2]
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. [3] [4] 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. [5]

In situations where it is not possible to assume a closed world for all predicates, yet some of them are known to be closed, the partial-closed world assumption can be used. This regime considers knowledge bases generally to be open, i.e., potentially incomplete, yet allows to use completeness assertions to specify parts of the knowledge base that are closed. [6]

See also

Related Research Articles

In artificial intelligence, the frame problem describes an issue with using first-order logic (FOL) to express facts about a robot in the world. Representing the state of a robot with traditional FOL requires the use of many axioms that simply imply that things in the environment do not change arbitrarily. For example, Hayes describes a "block world" with rules about stacking blocks together. In a FOL system, additional axioms are required to make inferences about the environment. The frame problem is the problem of finding adequate collections of axioms for a viable description of a robot environment.

Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and argument flow. Compound propositions are formed by connecting propositions by logical connectives. The propositions without logical connectives are called atomic propositions.

Inductive logic programming (ILP) is a subfield of symbolic artificial intelligence which uses logic programming as a uniform representation for examples, background knowledge and hypotheses. Given an encoding of the known background knowledge and a set of examples represented as a logical database of facts, an ILP system will derive a hypothesised logic program which entails all the positive and none of the negative examples.

In logic, negation, also called the logical complement, is an operation that takes a proposition to another proposition "not ", written , which is interpreted intuitively as being true when is false, and false when is true. Negation is thus a unary (single-argument) logical connective. It may be applied as an operation on notions, propositions, truth values, or semantic values more generally. In classical logic, negation is normally identified with the truth function that takes truth to falsity and vice versa. In intuitionistic logic, according to the Brouwer–Heyting–Kolmogorov interpretation, the negation of a proposition is the proposition whose proofs are the refutations of .

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not include the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

A non-monotonic logic is a formal logic whose consequence relation is not monotonic. In other words, non-monotonic logics are devised to capture and represent defeasible inferences, i.e., a kind of inference in which reasoners draw tentative conclusions, enabling reasoners to retract their conclusion(s) based on further evidence. Most studied formal logics have a monotonic consequence relation, meaning that adding a formula to a theory never produces a reduction of its set of consequences. Intuitively, monotonicity indicates that learning a new piece of knowledge cannot reduce the set of what is known. A monotonic logic cannot handle various reasoning tasks such as reasoning by default, abductive reasoning, some important approaches to reasoning about knowledge, and similarly, belief revision.

A paraconsistent logic is an attempt at a logical system to deal with contradictions in a discriminating way. Alternatively, paraconsistent logic is the subfield of logic that is concerned with studying and developing paraconsistent systems of logic.

Default logic is a non-monotonic logic proposed by Raymond Reiter to formalize reasoning with default assumptions.

Method of analytic tableaux

In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.

Belief revision is the process of changing beliefs to take into account a new piece of information. The logical formalization of belief revision is researched in philosophy, in databases, and in artificial intelligence for the design of rational agents.

The situation calculus is a logic formalism designed for representing and reasoning about dynamical domains. It was first introduced by John McCarthy in 1975. The main version of the situational calculus that is presented in this article is based on that introduced by Ray Reiter in 1991. It is followed by sections about McCarthy's 1986 version and a logic programming formulation.

Negation as failure is a non-monotonic inference rule in logic programming, used to derive from failure to derive . Note that can be different from the statement of the logical negation of , depending on the completeness of the inference algorithm and thus also on the formal logic system.

Circumscription is a non-monotonic logic created by John McCarthy to formalize the common sense assumption that things are as expected unless otherwise specified. Circumscription was later used by McCarthy in an attempt to solve the frame problem. To implement circumscription in its initial formulation, McCarthy augmented first-order logic to allow the minimization of the extension of some predicates, where the extension of a predicate is the set of tuples of values the predicate is true on. This minimization is similar to the closed-world assumption that what is not known to be true is false.

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic. In other words, iteratively applying the resolution rule in a suitable way allows for telling whether a propositional formula is satisfiable and for proving that a first-order formula is unsatisfiable. Attempting to prove a satisfiable first-order formula as unsatisfiable may result in a nonterminating computation; this problem doesn't occur in propositional logic.

Unit propagation (UP) or Boolean Constraint propagation (BCP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of clauses.

The autoepistemic logic is a formal logic for the representation and reasoning of knowledge about knowledge. While propositional logic can only express facts, autoepistemic logic can express knowledge and lack of knowledge about facts.

The Yale shooting problem is a conundrum or scenario in formal situational logic on which early logical solutions to the frame problem fail. The name of this problem derives from its inventors, Steve Hanks and Drew McDermott, working at Yale University when they proposed it. In this scenario, Fred is initially alive and a gun is initially unloaded. Loading the gun, waiting for a moment, and then shooting the gun at Fred is expected to kill Fred. However, if inertia is formalized in logic by minimizing the changes in this situation, then it cannot be uniquely proved that Fred is dead after loading, waiting, and shooting. In one solution, Fred indeed dies; in another solution, the gun becomes mysteriously unloaded and Fred survives.

The event calculus is a logical language for representing and reasoning about events and their effects first presented by Robert Kowalski and Marek Sergot in 1986. It was extended by Murray Shanahan and Rob Miller in the 1990s. Similar to other languages for reasoning about change, the event calculus represents the effects of actions on fluents. However, events can also be external to the system. In the event calculus, one can specify the value of fluents at some given time points, the events that take place at given time points, and their effects.

The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program completion and the well-founded semantics. The stable model semantics is the basis of answer set programming.

The paradoxes of material implication are a group of formulae that are truths of classical logic but are intuitively problematic.

References

  1. Reiter, Raymond (1978). "On Closed World Data Bases". In Gallaire, Hervé; Minker, Jack. Logic and Data Bases. Plenum Press. pp. 119–140. ISBN   9780306400605.
  2. Minker, Jack (1982), "On indefinite databases and the closed world assumption", 6th Conference on Automated Deduction, Lecture Notes in Computer Science, 138, Springer Berlin Heidelberg, pp. 292–308, doi:10.1007/BFb0000066, ISBN   978-3-540-11558-8
  3. Eiter, Thomas; Gottlob, Georg (June 1993). "Propositional circumscription and extended closed-world reasoning are Π 2 p ". Theoretical Computer Science. 114 (2): 231–245. doi : 10.1016/0304-3975(93)90073-3. ISSN 0304-3975.
  4. Lifschitz, Vladimir (November 1985). "Closed-world databases and circumscription". Artificial Intelligence. 27 (2): 229–235. doi : 10.1016/0004-3702(85)90055-4. ISSN 0004-3702.
  5. Cadoli, Marco; Lenzerini, Maurizio (April 1994). "The complexity of propositional closed world reasoning and circumscription". Journal of Computer and System Sciences. 48 (2): 255–310. doi : 10.1016/S0022-0000(05)80004-2. ISSN 0022-0000.
  6. Razniewski, Simon; Savkovic, Ognjen; Nutt, Werner (2015). "Turning The Partial-closed World Assumption Upside Down" (PDF).Cite journal requires |journal= (help)