Saturation, nonmonotonic reasoning and the closed-world assumption

摘要

To deal with the problem of implicit negative information in databases, it is necessary to use a nonmonotonic form of reasoning.The form of reasoning described in this paper uses an ordering relation on interpretations of the type: I is inferior to J if every ‘elementary fact’ true in I is true in J. In simple cases, this rule may be defined by: a set P of formulas implies a formula q if every minimal model of P satisfies q. In more general cases, this definition leads to paradox, if P is consistent and has no minimal model (P must not imply q and its negation).We have: 1.(1) carefully formulated the definition of a special type of implication (called ‘sub-implication’) to avoid this type of paradox;2.(2) proved that if P is a set of clauses, then P has a minimal model, and more generally that every model of a set of clauses is minored by one of its minimal models;3.(3) developed (in this last case subject to certain conditions such as the use of a particular set of clauses called groundable clauses or g-clauses) a decidable algorithm to compute whether P implies q, q being practically any formula.