Automatic Inference in Quantified Computational Logic

Abstract

A theory has been developed for reasoning about what is logically possible. The immediate motivation for this research is that advanced logic programming languages involved a nondeducibility primitive (THNOT is planner, one use of CUT in PROLOG) Which says to infer something if its negation is not deducible. The immediate significance of these results is that we now have effective axiomatizations for proving the correctness of logic programs involving non-deductibility primitives, and of various kinds of truth maintenance systems. However, the overall significance of this result transcends this particular application to program verification, because it provides the correct axiomatization of this concept, and much of the research on the logical representation of knowledge in artificial intelligence presupposes a solution to this very problem.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1988
Accession Number
ADA200909

Entities

People

  • Frank M. Brown

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Autonomy

DTIC Thesaurus Topics

  • Applied Mathematics
  • Artificial Intelligence
  • Automatic
  • Classification
  • Computer Programming
  • Language
  • Mathematics
  • Military Research
  • New York
  • Programming Languages
  • Reasoning
  • Rocky Mountains
  • Security
  • Software Design
  • Workshops

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.
  • Theoretical Analysis.

Technology Areas

  • AI & ML