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

The ECWA and the formalism of circumscription coincide on propositional theories. [5] [6] 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. [7]

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. [8]

Partial-closed world assumption

The language of logic programs with strong negation allows us to postulate the closed-world assumption for some statements and leave the other statements in the realm of the open-world assumption. [9] An intermediate ground between OWA and CWA is provided by the partial-closed world assumption (PCWA). Under the PCWA, the knowledge base is generally treated under open-world semantics, yet it is possible to assert parts that should be treated under closed-world semantics, via completeness assertions. The PCWA is especially needed for situations where the CWA is not applicable due to an open domain, yet the OWA is too credulous in allowing anything to be possibly true. [10] [11]

See also

Related Research Articles

In artificial intelligence, with implications for cognitive science, the frame problem describes an issue with using first-order logic to express facts about a robot in the world. Representing the state of a robot with traditional first-order logic 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 first-order logic 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.

<span class="mw-page-title-main">Negation</span> Logical operation

In logic, negation, also called the logical not or logical complement, is an operation that takes a proposition to another proposition "not ", standing for " is not true", written , or . It is interpreted intuitively as being true when is false, and false when is true. Negation is thus a unary 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. 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 assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies.

A non-monotonic logic is a formal logic whose conclusion 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 entailment relation, meaning that adding a formula to the hypotheses never produces a pruning of its set of conclusions. Intuitively, monotonicity indicates that learning a new piece of knowledge cannot reduce the set of what is known. Monotonic logics cannot handle various reasoning tasks such as reasoning by default, abductive reasoning, some important approaches to reasoning about knowledge, and similarly, belief revision.

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 "inconsistency-tolerant" systems of logic, which reject the principle of explosion.

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

<span class="mw-page-title-main">Method of analytic tableaux</span> Tool for proving a logical formula

In proof theory, the semantic tableau, also called an analytic tableau, truth tree, or simply tree, 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 1963. 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.

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

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.

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 comes from a scenario proposed by 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 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.

Abductive logic programming (ALP) is a high-level knowledge-representation framework that can be used to solve problems declaratively, based on abductive reasoning. It extends normal logic programming by allowing some predicates to be incompletely defined, declared as abducible predicates. Problem solving is effected by deriving hypotheses on these abducible predicates as solutions of problems to be solved. These problems can be either observations that need to be explained or goals to be achieved. It can be used to solve problems in diagnosis, planning, natural language and machine learning. It has also been used to interpret negation as failure as a form of abductive reasoning.

T-norm fuzzy logics are a family of non-classical logics, informally delimited by having a semantics that takes the real unit interval [0, 1] for the system of truth values and functions called t-norms for permissible interpretations of conjunction. They are mainly used in applied fuzzy logic and fuzzy set theory as a theoretical basis for approximate reasoning.

A non-normal modal logic is a variant of modal logic that deviates from the basic principles of normal modal logics.

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, vol. 138, Springer Berlin Heidelberg, pp. 292–308, doi:10.1007/BFb0000066, ISBN   978-3-540-11558-8
  3. Suchenek, Marek A. (1997), "Evaluation of Queries under Closed-World Assumption.", Kluwer Academic Publishers / Springer (18): 237–263, doi:10.1023/A:1005723423016
  4. Suchenek, Marek A. (2000), "Evaluation of Queries under Closed-World Assumption. Part II: The Hierarchical Case", Kluwer Academic Publishers / Springer (25): 247–289, doi:10.1023/A:1006319819647
  5. 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.
  6. 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.
  7. 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.
  8. Razniewski, Simon; Savkovic, Ognjen; Nutt, Werner (2015). "Turning The Partial-closed World Assumption Upside Down" (PDF).{{cite journal}}: Cite journal requires |journal= (help)
  9. Russell, Stuart J.; Norvig, Peter (2010). Artificial Intelligence: A Modern Approach (3rd ed.). Upper Saddle River: Prentice Hall.
  10. Motro (1989). "Integrity = Validity + Completeness".
  11. Razniewski, Simon; Savkovic, Ognjen; Nutt, Werner (2015). "Turning The Partial-closed World Assumption Upside Down" (PDF).