;; -*- Lisp -*-

;;; Natural deduction rules for TRE

;; Copyright (c) 1988, Kenneth D. Forbus, University of Illinois
;; All rights reserved.

;; These rules are based on a natural deduction system
;; developed by Kalish and Montigue, which organizes rules
;; in terms of introducing and eliminating connectives.
;; This provides a natural organization for our inference
;; rules.

;; As in the written rules, the predicate "SHOW" will indicate
;; our interest in a proving a fact of a particular form.

;; We begin by Modus ponens (conditional elimination)
;; and its friends.

(rule (implies ?p ?q) ;; conditional elimination
      (rule ?p (assert! ?q)))

(rule (show ?q) ;; backward chaining.
 (rule (implies ?p ?q)
  (unless (fetch ?q) (assert! `(show ,?p)))))

(rule (and . ?conjuncts) ;AND elimination
 (dolist (conjunct ?conjuncts)
    (assert! conjunct)))

(rule (show (and ?a ?b))
 (assert! `(show ,?a))
 (assert! `(show ,?b))
 (rule ?a (rule ?b (assert! `(and ,?a ,?b)))))

;;;; Biconditional elimination and introduction

(rule (iff ?p ?q) ;; IFF elimination
 (assert! `(implies ,?p ,?q))
 (assert! `(implies ,?q ,?p)))

(rule (show (iff ?p ?q)) ;IFF introduction
 (assert! `(show (implies ,?p ,?q)))
 (assert! `(show (implies ,?q ,?p)))
 (rule (implies ?p ?q)
  (rule (implies ?q ?p)
   (assert! `(iff ,?p ,?q)))))

(rule (not (not ?p))
 (assert! ?p)) ;; NOT elimination

;;;; Disjunction elimination and introduction

(rule (show (or ?a ?b)) ;; OR introduction
 (assert! `(show ,?a))
 (assert! `(show ,?b))
 (rule ?a (assert! `(or ,?a ,?b)))
 (rule ?b (assert! `(or ,?a ,?b))))
 
(rule (show ?r) ;; OR elimination
 (rule (or ?p ?q)
  (assert! `(show (implies ,?p ,?r)))
  (assert! `(show (implies ,?q ,?r)))
  (rule (implies ?p ?r)
   (rule (implies ?q ?r) (assert! ?r)))))