;; -*- Mode: Lisp; -*-

;;;; Laws of QP theory for TGizmo
;;;; File name: laws.lsp
;;;;  modified: Thursday, February 14, 2008 at 11:26:49 by Ken Forbus

;;; Copyright (c) 1991, Kenneth D. Forbus, Northwestern University,
;;;  and Johan de Kleer, the Xerox Corporation.
;;; All Rights Reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

;;; This file implements a subset of QP theory, using
;;; the LTMS to directly encode axiomatic statements.


(in-package :cl-user)

(rule ((:intern (quantity (?qtype ?individual)) :var ?qdecl))
      ;; Greatly restricted
      (rassert! (:implies ?qdecl (exists ?individual))
                :quantity-existence)
      (rassert! (set (dis (?qtype ?individual))) :dis-def)
      (rassert! (set (iis (?qtype ?individual))) :iis-def)
      (push (list ?qtype ?individual) (tgizmo-quantities *tgizmo*)))

;;; In the next five rules, 
;;;    ?n1, ?n2 = (<A or D> (?qtype ?individual)) | <constant>

(rule ((:intern (> ?n1 ?n2) :var ?gt))
      (install-comparison-constraints-if-needed ?n1 ?n2)
      (rassert! (:iff ?gt (:and (?n2 <= ?n1)
				(:not (?n1 <= ?n2))))
                :>-def))

(rule ((:intern (< ?n1 ?n2) :var ?lt))
      (install-comparison-constraints-if-needed ?n1 ?n2)
      (rassert! (:iff ?lt (:and (?n1 <= ?n2)
				(:not (?n2 <= ?n1))))
		:<-def))

(rule ((:intern (= ?n1 ?n2) :var ?eq))
      (install-comparison-constraints-if-needed ?n1 ?n2)
      (rassert! (:iff ?eq (:and (?n1 <= ?n2)
				(?n2 <= ?n1)))
		:=-def))

(rule ((:intern (>= ?n1 ?n2) :var ?gte))
      (install-comparison-constraints-if-needed ?n1 ?n2)
      (rassert! (:iff ?gte (?n2 <= ?n1)) :>=-def))

(rule ((:intern (<= ?n1 ?n2) :var ?lte))
      (install-comparison-constraints-if-needed ?n1 ?n2)
      (rassert! (:iff ?lte (?n1 <= ?n2)) :<=-def))

;;;; Accumulating process and view structures

(rule ((:true (active ?p) :var ?aform))
      ;; If active, it's in there.
      (rule ((:true (process-instance ?p) :var ?pform))
	    (rassert! (:implies (:and ?pform ?aform)
				(ps has-member ?p))
		      :ps-member))
      (rule ((:true (view-instance ?p) :var ?pform))
	    (rassert! (:implies (:and ?pform ?aform)
				(vs has-member ?p))
		      :vs-member)))

(rule ((:false (active ?p) :var ?aform))
      ;; If inactive, it's known to not be in there.
      (rule ((:true (process-instance ?p) :var ?pform))
	    (rassert! (:implies (:and ?pform (:not ?aform))
				(:not (ps has-member ?p)))
		      :not-ps-member))
      (rule ((:true (view-instance ?p) :var ?pform))
	    (rassert! (:implies (:and ?pform (:not ?aform))
				(:not (vs has-member ?p)))
		      :not-vs-member)))

;;;; Accumulating influences

(rule ((:intern (quantity ?q) :var ?qform))
      (rassert! (:iff (:or (:not ?qform) ((dis ?q) members nil))
		      (:not (directly-influenced ?q)))
		:dis-definition)
      (rassert! (:iff (:or (:not ?qform) ((iis ?q) members nil))
		      (:not (indirectly-influenced ?q)))
		:iis-definition)
      (rassert! (:not (:and ?qform
			    (directly-influenced ?q)
			    (indirectly-influenced ?q)))
		:qp-consistency-law)
      (rassert! (:implies (:and ?qform
				(:not (directly-influenced ?q))
				(:not (indirectly-influenced ?q)))
			  (= (d ?q) zero))
		:uninfluenced-definition))

(rule ((:true (i+ ?influenced ?influencer ?source) :var ?is))
      (rassert! (:implies ?is (directly-influenced ?influenced))
		:dis-definition)
      (rassert! (:iff ?is ((dis ?influenced) has-member ?is))
		:dis-definition))

(rule ((:true (i- ?influenced ?influencer ?source) :var ?is))
      (rassert! (:implies ?is (directly-influenced ?influenced))
		:dis-definition)
      (rassert! (:iff ?is ((dis ?influenced) has-member ?is))
		:dis-definition))

(rule ((:true (qprop ?influenced ?influencer ?source) :var ?is))
      (rassert! (:implies ?is (indirectly-influenced ?influenced))
		:iis-definition)
      (rassert! (:iff ?is ((iis ?influenced) has-member ?is))
		:iis-definition))

(rule ((:true (qprop- ?influenced ?influencer ?source) :var ?is))
      (rassert! (:implies ?is (indirectly-influenced ?influenced))
		:iis-definition)
      (rassert! (:iff ?is ((iis ?influenced) has-member ?is))
		:iis-definition))