Report Number: CS-TR-77-618
Institution: Stanford University, Department of Computer Science
Title: A production system for automatic deduction
Author: Nilsson, Nils J.
Date: August 1977
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 untll 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.