BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-77-618
       ENTRY:: June 28, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: A production system for automatic deduction
        TYPE:: Technical Report
      AUTHOR:: Nilsson, Nils J.
        DATE:: August 1977
       PAGES:: 54
    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.
       NOTES:: [Adminitrivia V1/Prg/19950628]
         END:: STAN//CS-TR-77-618