A Production System for Automatic Deduction

Abstract

A new predicate calculus deduction system based on production rules is proposed. The system combines several developments in Artificial Intelligence and Automatic Theorem Proving research including the use of domain-specific inference rules and separate mechanisms for forward and backward reasoning. It has a clean separation between the data base, the production rules, and the control system. Goals and subgoals are maintained in an AND/OR tree to represent assertions. The production rules modify these structures until they 'connect' in a fashion that proves the goal theorem. Unlike some previous systems that used production rules, ours is not limited to rules in Horn Clause form. Unlike previous PLANNER-like systems, ours can handle the full range of predicate calculus expressions including those with quantified variables, disjunctions and negations.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1977
Accession Number
ADA045948

Entities

People

  • Nils J. Nilsson

Organizations

  • Stanford University

Tags

Communities of Interest

  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Automatic
  • Calculus
  • Cognitive Science
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Consistency
  • Control Systems
  • Conversion
  • Databases
  • Information Processing
  • Language
  • New York
  • Production
  • United States

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • AI & ML
  • AI & ML - Bayesian Inference
  • AI & ML - Information Retrieval
  • AI & ML - Machine Translation