Хроника ИИ

Источники

• Negation as Failure ↗
  Подтверждающий фрагмент

  Negation as Failure Keith L. Clark Hervé Gallaire, Jack Minker (eds.) Logic and Data Bases, pages 293–322 Springer, Boston, MA 1978 A query evaluation process for a logic data base comprising a set of clauses is described. It is essentially a Horn clause theorem prover augmented with a special inference rule for dealing with negation. This is the negation as failure inference rule whereby ~P can be inferred if every possible proof of P fails. The chief advantage of the query evaluator described

• Logic Programming ↗
  Подтверждающий фрагмент

  solving a negative goal not B is interpreted as reasoning with ¬B. But in most proof theories, not B is interpreted as some form of negation as failure: not B holds if all attempts to show B fail. In addition to these purely logical problems concerning semantics and proof theory, LP has been plagued by controversies concerning declarative versus procedural representations. Declarative representations are naturally supported by bottom- up model generation. But both declarative and procedural repr

• Logic Programming ↗
  Подтверждающий фрагмент

  importantly because they fail to capture non-monotonic reasoning. For non-monotonic reasoning, it is necessary to extend Horn clauses to clauses of the form: A0 ← A1 ∧ ... ∧ An ∧ not B1 ∧ ... ∧ not Bm where n ≥ 0 and m ≥ 0. Each Ai and Bi is an atomic formula, and “not” is read as not. Atomic formulas and their negations are also called literals. Here the Ai are positive literals, and the not Bi are negative literals. Sets of clauses in this form are called normal logic programs, or just logic p