;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - NFS Share File - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(in-package 'user :use '(lisp))

;This code depends on the files util.lisp, and unify.lisp.

;Anyone reading this file should first read the paper
;``automatic recongition of tractability in inference relations''

;This is an example of locality testing using the functions in this
;file.
;
;Other tests are contained at the end of this file.
;
;(defun monotone-test ()
;
;  (system-init)
;
;  (type-declarations
;    (?x D)         ;?x : D
;    (?y D)
;    (?z D)
;    (is ((D D) B)) ;is : D X D -> B
;    (f ((D) D)))   ;f  : D -> D
;
;  (rule nil
;    (is ?x ?x))
;
;  (rule ((is ?x ?y)
;         (is ?y ?z))
;    (is ?x ?z))
;
;  (rule ((is ?x ?y))
;    (is (f ?x) (f ?y)))
;
;  (examine-rules))

;The procedure examine-rules prints information as it checks the locality of
;the rule set.  For example

;(monotone-test)

;there are 4 rank 0 templates
;there are no rank 0 feedback events

;there are 3 rank 1 templates
;thera are no rank 1 feedback events

;there are 2 rank 2 templates
;there are no rank 2 feedback events

;there are no rank 3 templates
;the given rules are 2 bounded local

;If you wish to examine the templates of a given rank you can type

;(templates-of-rank 2)
;
;((TEMPLATE 47
;	   (ALPHA IS (F ?C))
;	   (SIGMA IS ((IS (F ?A) ?B) (IS ?C ?A)))
;	   (PHI IS (IS (F ?C) ?B)))
; (TEMPLATE 88
;	   (ALPHA IS (F ?C))
;	   (SIGMA IS ((IS ?A ?C) (IS ?B (F ?A))))
;	   (PHI IS (IS ?B (F ?C)))))


;You can also access templates directly by number using the procedure tn.

;(tn 88)
;
;(TEMPLATE 88
;	  (ALPHA IS (F ?C))
;	  (SIGMA IS ((IS ?A ?C) (IS ?B (F ?A))))
;	  (PHI IS (IS ?B (F ?C))))
;
;As another example consider the following test (defined at the end of the file)
;
;(monotone-test2)
;
;...
;
;templates (86 126) are feedback events
;the given rules are not local
;
;(tn 86)
;
;(TEMPLATE 86
;	  (ALPHA IS (F ?D ?C))
;	  (SIGMA IS ((IS ?D ?A) (IS ?B ?C)))
;	  (PHI IS (IS (F ?D ?B) (F ?A ?C))))

;
(defvar *rules* nil)
(defvar *rule-count* 0)
(defvar *rule-table* nil)
(defvar *types* nil)
(defvar *constants* nil)
(defvar *node-count* 0)
(defvar *node-table* (make-hash-table :test #'equal))
(defvar *old-nodes* nil)
(defvar *nodes* nil)
(defvar *grules* nil)
(defvar *ever-upsilon-nodes* nil)
(defvar *semmod-vars* nil)
(defvar *closed-rules* nil)

(defun system-init ()
  (setq *rules* nil)
  (setq *rule-count* 0)
  (setq *rule-table* (make-array 100))
  (setq *types* nil)
  (setq *constants* nil)
  
  (setq *node-count* 0)
  (setq *node-table* (make-hash-table :test #'equal))

  (setq *old-nodes* nil)
  (setq *nodes* nil)
  (setq *grules* nil)
  (setq *ever-upsilon-nodes* nil)
  (setq *semmod-vars* nil)
  (setq *closed-rules* nil))




(defmacro rn (n)
  `(aref *rule-table* ,n))

(defstruct (rule (:print-function (lambda (self stream &rest ignore)
				    (format stream "[rule ~s ~s ~s]"
						(rule-number self)
						(rule-body self)
						(rule-head self)))))
  head
  body
  number
  covering-expressions)

(defun rule-variables (rule)
  (variables (cons (rule-head rule) (rule-body rule))))

(defmacro rule (body &body head)
  `(rule-fun ',(car head) ',body))

(defmacro new-rule (head &body  body)
  `(make-new-rule ',head ',body))

(defun rule-fun (head body)
  (examine-expression head)
  (mapc #'examine-expression body)
  (unless (and (eq 'b (expression-type head))
	       (every (lambda (ant) (eq 'b (expression-type ant)))
		      body))
    (error "some rule component in ~s ~s is not of type Boolean"
	   body head))
  (selectmatch (alpha-rename (list head body))
    ((?head ?body)
     (push (make-new-rule ?head ?body) *rules*))))

(defun make-new-rule (head body)
  (let ((rule (make-rule :head head :body body :number (incf *rule-count*))))
    (setf (rn (rule-number rule)) rule)
    (compute-covering-expressions rule)
    rule))

(defun compute-covering-expressions (rule)
  (let ((variables (rule-variables rule))
	(subexpressions (remove-duplicates
			  (mapcan (lambda (exp)
				    (when (consp exp)
				      (copy-list (remove-if-not 'variables exp))))
				  (cons (rule-head rule)
					(rule-body rule))))))
    (dolist (var variables)
      (when (not (some (lambda (subexpression)
			 (member var (variables subexpression)))
		       subexpressions))
	(error "~s in the rule ~s is illegal --- use the special constant (false)"
	       var
	       rule)))
    (setf (rule-covering-expressions rule)
	  (compute-cover2 variables subexpressions))))

(defun compute-cover2 (variables subexps)
  (dotimes (n (1+ (length variables)))
    (let ((cover (compute-cover3 variables subexps n)))
      (unless (eq cover 'fail)
	(return-from compute-cover2 cover))))
  (error "this should never happen"))

(defun compute-cover3 (variables subexps cover-size)
  (cond ((= cover-size 0)
	 (if (null variables)
	     nil
	     'fail))
	(t
	 (dolist (subexp subexps)
	   (let ((rest (compute-cover3 (set-difference variables (variables subexp))
				       subexps
				       (1- cover-size))))
	     (unless (eq rest 'fail)
	       (return-from compute-cover3 (cons subexp rest)))))
	 'fail)))

(defun examine-expression (exp)
  (let ((type (expression-type exp)))
    (pushnew type *types* :test #'equal)
    (when (listp exp)
      (dolist (subexp exp)
	(unless (variables subexp)
	  (pushnew subexp *constants* :test #'equal))
	(examine-expression subexp)))))


(defvar *current-rank*)

(defvar *template-count*)

(defvar *old-templates*)

(defvar *new-templates*)

(defvar *alpha-vars*)

(defvar *template-table* (make-array 100000))

(defvar *template-rank-table* (make-array 1000))

(defun templates-of-rank (r)
  (mapcar 'template-expression
	  (aref *template-rank-table* r)))

(defvar *max-rank* 0)

(defun examine-rules ()
  (dotimes (n 100000)
    (setf (aref *template-table* n) nil))
  (gensym 1)

  (let ((*template-count* 0)
	(*old-templates* nil)
	(*new-templates* nil)
	(*alpha-vars* (mapcar (lambda (type)
				(let ((var (gensym "?ALPHA-")))
				  (make-declaration var type)
				  var))
			      *types*)))

    ;initialize *new-templates* to null templates
    (let ((phi (gensym "?PHI-")))
      (make-declaration phi 'b)
      (dolist (alpha *alpha-vars*)
	(declare-template nil nil alpha phi (list phi) nil nil)))

    (setf *max-rank* 0)
    (process-rank 0)))

(defun process-rank (rank)
  (format t "~% Filtering New Templates")
  (let ((filtered-new-templates nil))
    (dolist (temp *new-templates*)
      (unless (some (lambda (template2) (covers? template2 temp))
		    *old-templates*)
	(setq filtered-new-templates
	      (cons temp
		    (remove-if (lambda (template2) (covers? temp template2))
			       filtered-new-templates)))
	(setq *old-templates*
	      (cons temp
		    (remove-if (lambda (template2) (covers? temp template2))
			       *old-templates*)))))
    (cond ((null filtered-new-templates)
	   (format t "~% ~% There are no templates of rank ~s" rank)
	   (format t "~% The given rules are ~s-bounded local ~%" (1- rank)))
	  (t
	   (format t "~% ~% There are ~s rank ~s templates"
		   (length filtered-new-templates)
		   rank)
	   (setf (aref *template-rank-table* rank) (copy-list filtered-new-templates))
	   (setf *max-rank* rank)
	   (let ((feedbacks (remove-if-not 'feedback-template? filtered-new-templates)))
	     (cond (feedbacks
		    (format t "~% Templates ~s are feedback events"
			    (mapcar 'template-number feedbacks))
		    (format t "~% The given rules are not local ~%"))
		   (t
		    (format t "~% There are no rank ~s feedback events ~%" rank)
		    (setq *new-templates* nil)
		    (process-rules filtered-new-templates)
		    (process-rank (1+ rank)))))))))

(defun process-rules (new-templates)
  (format t "~% Generating New Templates")
  (dolist (rule *rules*)
    (dolist (alpha *alpha-vars*)
      (check-forward rule alpha new-templates))))

;when this function is called new-templates is a subset of *old-templates*

(defun check-forward (rule alpha new-templates)
  (labels ((check-forward2 (used antecedents sigma upsilon subst)
	     (if (null antecedents)
		 ;rules without antecedents are allowed when the subset test is true.
		 (when (or (subsetp *old-templates* new-templates)
			   (some (lambda (used-template) (member used-template new-templates))
				 used))
		   (construct-arg-cases rule used alpha (rule-head rule) sigma upsilon subst))
		 (dolist (template *old-templates*)
		   ;alpha-renaming is required to handled repetations of the same template
		   (selectmatch (alpha-rename (list (template-alpha template)
						    (template-phi template)
						    (template-sigma template)
						    (template-upsilon template)))
		     ((?alpha ?phi ?sigma ?upsilon)
		      (let ((subst2 (unify (cons alpha (car antecedents))
						(cons ?alpha ?phi)
						subst)))
			(unless (eq subst2 'fail)
			  (check-forward2  (cons template used)
					   (cdr antecedents)
					   (append ?sigma sigma)
					   (append ?upsilon upsilon)
					   subst2)))))))))
    (check-forward2 nil (rule-body rule) nil nil nil)))

;In the following it is safe to accumulate a substitution.

(defun construct-arg-cases (rule used-templates alpha phi sigma upsilon subst)
  (if (symbolp phi)
      (declare-template rule used-templates alpha phi sigma upsilon subst)
      (labels ((cases2 (subexps upsilon subst)
		 (cond ((null subexps)
			(declare-template rule used-templates alpha phi sigma upsilon subst))
		       (t
			(let ((subst2 (unify (car subexps) alpha subst)))
			  (unless (equal subst2 'fail)
			    (cases2 (cdr subexps) upsilon subst2)))
			(cases2 (cdr subexps) (cons (car subexps) upsilon) subst)))))
	(cases2 phi upsilon subst))))


(defun tn (n)
  (template-expression (aref *template-table* n)))


(defstruct (template (:print-function (lambda (template stream &rest ignore)
				    (format stream "[template ~s ~s ~s ~s]"
					    (template-number template)
					    (template-alpha template)
					    (template-phi template)
					    (template-sigma template)))))
  number
  alpha
  phi
  sigma
  upsilon
  (cache-flag nil)
  sigma-closure-cache
  source-rule
  source-templates)

(defun rename-variables (variables names)
  (and variables
       (progn (if (null names)
		  (error "more variables than names in rename-variables"))
	      (acons (car variables)
		     (car names)
		     (rename-variables (cdr variables) (cdr names))))))

(defvar *names* '(?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k ?l ?m ?n ?o ?p ?q ?r ?s ?t))

(defun alpha-simplify (expression)
  (let ((alist (rename-variables (variables expression) *names*)))
    (sublis alist expression)))

(defun template-rank (template)
  (cond ((null (template-source-rule template)) 0)
	((null (template-source-templates template)) 1)
	(t (1+ (apply #'max (mapcar 'template-rank (template-source-templates template)))))))

(defun template-expression (template)
  (alpha-simplify `(template ,(template-number template)
			     (alpha is ,(template-alpha template))
			     (sigma is ,(template-sigma template))
			     (phi is ,(template-phi template)))))

(defun label-formula? (phi upsilon)
  (or (symbolp phi)
      (every (lambda (arg) (equal-member arg upsilon))
	     phi)))

(defun feedback-template? (template)
  (and (label-formula? (template-phi template) (template-upsilon template))
       (not (cr-member? (template-phi template) template))))

(defun template-sigma-closure (template)
  (unless (template-cache-flag template)
    (setf (template-sigma-closure-cache template)
	  (cr (template-sigma template) (template-upsilon template)))
    (setf (template-cache-flag template) t))
  (template-sigma-closure-cache template))

(defun cr-member? (phi template)
  (let ((closure (template-sigma-closure template)))
    (or (equal-member phi closure)
	(and (universal? closure) (symbolp phi)))))

;The generic formula is included in a closure iff the closure is universal
;(equals all label formulas of Upsilon)

(defvar *generic-formula* (gensym "P-"))
(make-declaration *generic-formula* 'B)

(defun universal? (closure)
  (member *generic-formula* closure))

(defun declare-template (source-rule source-templates alpha phi sigma upsilon subst)
  (let ((template (make-template :number (incf *template-count*))))
    (setf (aref *template-table* (template-number template)) template)
    (setf (template-source-rule template) source-rule)
    (setf (template-source-templates template) (reverse source-templates))
    (selectmatch (alpha-rename (apply-subst subst (list alpha phi sigma upsilon)))
      ((?alpha ?phi ?sigma ?upsilon)
       (setf (template-alpha template) ?alpha)
       (setf (template-phi template) ?phi)
       (setf (template-sigma template) (remove-duplicates ?sigma :test #'equal))
       (setf (template-upsilon template)
	     (upsilon-closure (append (when (consp ?alpha) ?alpha)
				      (mapcan (lambda (psi)
						(when (consp psi) (copy-list psi)))
					      ?sigma)
				      ?upsilon)))
        (unless (equal-member (template-alpha template)
			      (template-upsilon template))
	 (push template *new-templates*))
       template))))


(defun upsilon-closure (terms)
  (remove-duplicates (cons *generic-formula*
			   (append *constants* (mapcan #'subterms terms)))
		     :test #'equal))

(defun subterms (term)
  (if (consp term)
      (cons term (mapcan #'subterms (cdr term)))
      (list term)))






(defun covers? (template1 template2)
  (let ((subst (match (list (template-alpha template1) (template-phi template1))
			    (list (template-alpha template2) (template-phi template2)))))
    (and (not (eq subst 'fail))
	 (covers2? template1 template2 subst))))

(defun covers2? (template1 template2 subst)
  (match-subset? (template-upsilon template1)
		 (template-upsilon template2)
		 subst
		 (lambda (subst2)
		   (or (eq 'universal (template-sigma-closure template2))
		       (match-cr-subset? (template-sigma template1)
					 (template-sigma-closure template2)
					 subst2)))))

;(defun paired-subsets? (list1 list2 subst)
;  (or (null list1)
;      (match-subset? (car list1)
;		     (car list2)
;		     (car tests)
;		     subst
;		     (lambda (subst2)
;		       (paired-subsets? (cdr list1) (cdr list2) subst2)))))

(defun match-subset? (set1 set2 subst continuation)
  (labels ((subset2? (set1 subst2)
	     (if (null set1)
		 (funcall continuation subst2)
		 (some (lambda (member2)
			 (let ((subst3 (match (first set1) member2 subst2)))
			   (and (not (eq subst3 'fail))
				(subset2? (cdr set1) subst3))))
		       set2))))
    (subset2? set1 subst)))

(defun match-cr-subset? (sigma1 closure2 subst)
  (labels ((subset2? (sigma1 subst2)
	     (or (null sigma1)
		 (if (and (symbolp (first sigma1))
			  (universal? closure2))
		     (subset2? (cdr sigma1) subst2)
		     (some (lambda (member2)
			     (let ((subst3 (match (first sigma1) member2 subst2)))
			       (and (not (eq subst3 'fail))
				    (subset2? (cdr sigma1) subst3))))
			   closure2)))))
    (subset2? sigma1 subst)))



;The function cr is the performance bottleneck of the system.
;Implementing cr requires implementing a theorem prover for the
;the given inference rules.  This implementation uses upsilon
;to convert the given rules into Boolean Horn clauses which can
;then be run in a forward chaining manner very efficiently.

;A node is a data structure that represents an
;expression.  Unlike list-structure repsentations, node representations
;have the property that equal expressions are eq objects.

;Various kinds of nodes need various kinds of slots -- we just include
;all the slots in the basic data structure.

(defstruct (node (:print-function (lambda (self stream &rest ignore)
					  (format stream "[node ~s ~s]"
						  (node-number self)
						  (unparse self)))))
  ;invariant slots
  number
  key
  rules-forward
  type

  ;set-once slot
  ever-upsilon?

  ;state-dependent slots
  (truth :unknown)
  binding
  upsilon?)

(defun new-node ()
  (let ((node (make-node :number (incf *node-count*))))
    (push node *nodes*)
    node))

(defun clear-nodes ()
  (dolist (node *nodes*)
    (setf (node-truth node) :unknown)
    (setf (node-binding node) nil)
    (setf (node-upsilon? node) nil)))



;We now give the basic Boolean inference engine.

;A Boolean rule is represented by a grule structure.

(defstruct (grule (:print-function
		    (lambda (rule stream &rest ignore)
		      (format stream "[grule ~s ~s]"
			      (node-key (grule-head rule))
			      (mapcar (lambda (ant) (node-key ant))
				      (grule-antecedents rule))))))

  ;invariant slots
  antecedents
  head
  acount

  ;state-dependent slots
  antecedent-count)

;the head and members of the body of a grule must each be
;label-formula data structures.

(defun add-rule (head body)
  (let* ((rule (make-grule :head head
			   :antecedents body)))
    (let ((acount 0))
      (dolist (ant body)
	(push rule (node-rules-forward ant))
	(incf acount))
      (setf (grule-acount rule)
	    acount))
    (push rule *grules*)
    rule))

;the following function allows a given set of grules to be used
;for more than one inference problem.

(defun clear-grules ()
  (dolist (rule *grules*)
    (setf (grule-antecedent-count rule) (grule-acount rule))))

(defun fire-null-grules ()
  (dolist (rule *grules*)
    (when (null (grule-antecedents rule))
      (assert-label (grule-head rule)))))

;To derive a formula a formula we must ensure that it is a labe formula
;of Upsilon.

(defun assert-label (label)
  (when (not (eq (node-type label) 'b))
    (error "asserting a non-formula"))
  (when (and (eq (node-truth label) :unknown)
	     (let ((key (node-key label)))
	       (or (symbolp key)
		   (every #'node-upsilon? key))))
    (setf (node-truth label) :true)
    (mapc 'propagate-through (node-rules-forward label))
    t))

(defun propagate-through (rule)
  (let ((new-a-count (decf (grule-antecedent-count rule))))
    (when (zerop new-a-count)
      (assert-label (grule-head rule)))))



;The following code creates grules form a set of normal (quantified)
;rules and a set of nodes.
;The creation of Boolean rules is incremental so that
;process-new-nodes can be called many
;different times with additional new nodes.  Only elements
;of Upsilon need be processed.

(defun add-to-upsilon! (node)
  (setf (node-upsilon? node) t)
  (when (not (node-ever-upsilon? node))
    (generate-grules node)))

;grule generation is the bottleneck of the cr function on large problems
;and thus the bottleneck of the whole system on large problems.
;Some of the complexity of grule generation is due to efficiency
;heuristics.  The following code generates n^2 grules for the
;substitution rule independent of the number of variables in the rule.
;A naive implementation of the binary subsitution rule gives n^4
;grule creations.

(defun generate-grules (node)
  (push node *ever-upsilon-nodes*)
  (setf (node-ever-upsilon? node) t)
  (dolist (rule *rules*)
    (generate-grules2 rule node)))

(defun generate-grules2 (rule new-node)
  (let ((cover-exps (rule-covering-expressions rule)))
    (when cover-exps
      (labels ((recurse (rest-exps subst new-node-used?)
		 (if (null rest-exps)
		     (generate-grules3 rule subst)
		     (let ((candidates (if (and (null (cdr rest-exps))
						(not new-node-used?))
					   (list new-node)
					   *ever-upsilon-nodes*)))
		       (dolist (n candidates)
			 (let ((subst2 (match (car rest-exps)
						    (unparse n)
						    subst)))
			   (unless (eq subst2 'fail)
			     (recurse (cdr rest-exps) subst2 (or new-node-used?
								  (eq n new-node))))))))))
	(recurse (rule-covering-expressions rule) nil nil)))))

(defun generate-grules3 (rule subst)
  (let ((hnode (parse (apply-match subst (rule-head rule))))
	(bnodes (mapcar (lambda (phi)
			  (parse (apply-match subst phi)))
			(rule-body rule))))
    (add-rule hnode bnodes)))



;The conversion of an expression to a node is complicated.
;A semantic modulation
;scheme is used to re-use previously constructed Boolean rules.
;A single node can be used to represent different
;expressions on different calls to the therorem prover.
;A new call to the theorem prover may not create any new nodes
;or Boolean rules.
;While re-using the Boolean rule data structures the marking
;package is used to mark those objects whose state is appropriated
;updated for the current call the procedure.

(defun parse-upsilon-member (expression)
  (let ((result (parse-internal expression 'parse-upsilon-member)))
    (add-to-upsilon! result)
    result))

(defun parse (expression)
  (parse-internal expression 'parse))

(defun parse-internal (expression recurse-fun)
  (cond ((variable? expression)
	 (semmod-bound-to expression))
	((typep expression 'node)
	 expression)
	((and (symbolp expression)
	      (get expression 'semmod-node))
	 (get expression 'semmod-node))
	(t
	 (let ((key (if (consp expression)
			(mapcar recurse-fun expression)
			expression)))
	   (or (gethash key *node-table*)
	       (let ((node (new-node)))
		 (setf (gethash key *node-table*) node)
		 (setf (node-type node)
		       (if (symbolp key)
			   (expression-type key)
			   (combination-type
			     (mapcar 'node-type key))))
		 (setf (node-key node) key)
		 node))))))

(defun unparse (node)
  (or (node-binding node)
      (if (consp (node-key node))
	  (mapcar #'unparse (node-key node)))
      (node-key node)))

(defun semmod-bound-to (symbol)
  (or (find-if (lambda (var) (eq symbol (node-binding var)))
	       *semmod-vars*)
      (let ((new-binding (get-unbound-var (expression-type symbol))))
	(setf (node-binding new-binding) symbol)
	new-binding)))

(defun get-unbound-var (type)
  (or (find-if (lambda (var) (and (null (node-binding var))
				  (eq (node-type var) type)))
	       *semmod-vars*)
      (new-semmod-var type)))

(defun new-semmod-var (type)
  (let ((node (new-node)))
    (setf *semmod-vars* (nconc *semmod-vars* (list node))) ;an efficiency heuristic
    (let ((symbol (gensym "SEMMOD-VAR-")))
      (setf (node-key node) symbol)
      (setf (get symbol 'semmod-node) node)
      (setf (node-type node) type)
      (make-declaration symbol type)
      node)))



;Finally, the function cr can be built on all of the above machinery.

(defun cr (sigma upsilon)

  (dolist (rule *rules*)
    (when (and (not (member rule *closed-rules*))
	       (null (rule-variables rule)))
      (add-rule (parse (rule-head rule))
		(mapcar 'parse (rule-body rule)))
      (push rule *closed-rules*)))

  (clear-nodes)
  (install-upsilon upsilon)
  (clear-grules)

  (fire-null-grules)
  (mapc (lambda (form) (assert-label (parse form)))
	sigma)

  (current-closure))

(defun install-upsilon (upsilon)
  (mapc #'parse-upsilon-member
	(sort (copy-list upsilon) 'larger-exp)))

(defun current-closure ()
  (if (and (equal (get 'false 'symbol-type) '(() b))
	   (eq :true (node-truth (parse '(false)))))
      'universal
      (mapcar 'unparse
	      (remove-if (lambda (node)
			   (eq :unknown (node-truth node)))
			 *nodes*))))

(defun larger-exp (exp1 exp2)
  (> (exp-weight exp1) (exp-weight exp2)))

(defun exp-weight (exp)
  (if (consp exp)
      (+ (exp-weight (car exp))
	 (exp-weight (cdr exp)))
      1))

;
;Contrapositives
;When using contrapositive type declarations ``not'' and ``false''
;are automatically provided.

(defvar *formulas* nil)

(defmacro contrapositive-type-declarations (&body declarations)
  (let ((*formulas* nil))
    `(progn (type-declarations
	      ,@(mapcan 'make-negation declarations)
	      (false (() B))
	      (not ((B) B))
	      (?p B))
	    ,@(mapcan 'predicate-rules *formulas*))))

(defun make-negation (declaration)
  (selectmatch declaration
    ((?constructor (?arg-types ?output-type))
     (if (not (eq ?output-type 'B))
	 (list declaration)
	 (let* ((variable-decls (mapcar (lambda (arg-type)
					  (list (gensym "?X-") arg-type))
					?arg-types))
		(variables (mapcar 'car variable-decls)))
	   (push (cons ?constructor variables) *formulas*)
	   (list* declaration
		  `(,(create-name 'not ?constructor) (,?arg-types ,?output-type))
		  variable-decls))))
    (:anything (list declaration))))

(defun predicate-rules (formula)
  (let ((not-formula `(,(create-name 'not (car formula)) ,@(cdr formula))))
    `((rule ((not ,formula))
	,not-formula)
      (rule (,not-formula)
	(not ,formula))
      (rule (,not-formula
	     ,formula)
	(false)))))

(defmacro multirule (antecedents &body conclusion)
  (setf conclusion (car conclusion))
  (let ((rule-pairs (cons (cons antecedents conclusion)
			  (mapcar (lambda (ant)
				    (cons (cons `(not ,conclusion)
						(remove ant antecedents))
					  `(not ,ant)))
				  antecedents))))
    `(progn ,@(mapcar 'make-clean-rule rule-pairs))))

(defun make-clean-rule (rule-pair)
  (let ((antecedents (mapcar 'remove-nots (car rule-pair)))
	(conclusion (remove-nots (cdr rule-pair))))
    `(rule ,antecedents
       ,conclusion)))

(defun remove-nots (formula)
  (selectmatch formula
    ((not (not ?form2))
     (remove-nots ?form2))
    ((not ?form2)
     (cons (create-name 'not (car ?form2)) (cdr ?form2)))
    (:anything
      formula)))


;Examples

(defun monotone-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (f ((D) D)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (f ?x) (f ?y)))

  (examine-rules))

(defun monotone-test2 ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (f ((D D) D)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (f ?x ?z) (f ?y ?z)))

  (rule ((is ?x ?y))
    (is (f ?z ?x) (f ?z ?y)))

  (examine-rules))

(defun induction-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (?R R)
    (apply ((R D) D))
    (apply* ((R D) D))
    (preserves ((R D) B)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (apply ?r ?x) (apply ?r ?y)))

  (rule ((is ?x ?y))
    (is (apply* ?r ?x) (apply* ?r ?y)))

  (rule ((is ?x ?y)
	 (is (apply ?r ?y) ?x))
    (preserves ?r ?x))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply ?r ?x) ?y))

  (rule ((is ?x ?y)
	 (is ?y ?x)
	 (preserves ?r ?x))
    (preserves ?r ?y))

  (rule ()
    (is ?x (apply* ?r ?x)))

  (rule ()
    (preserves ?r (apply* ?r ?x)))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply* ?r ?x) ?y))

  (examine-rules))

(defun contrapositive-monotone-test ()

  (system-init)

  (contrapositive-type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (f ((D) D)))

  (multirule nil
	     (is ?x ?x))

  (multirule ((is ?x ?y)
	      (is ?y ?z))
	     (is ?x ?z))

  (multirule ((is ?x ?y))
	     (is (f ?x) (f ?y)))

  (examine-rules))

(defun Boolean-test ()

  (system-init)

  (type-declarations
    (?P B)
    (?Q B)
    (false (() B))
    (or ((B B) B))
    (not ((B) B)))

  (RULE ((NOT (NOT ?P)))
    ?P)

  (RULE (?P)
    (NOT (NOT ?P)))

  (RULE ((OR ?P ?Q)
	 (NOT ?P))
    ?Q)

  (RULE ((OR ?P ?Q)
	 (NOT ?Q))
    ?P)

  (RULE (?P)
    (OR ?P ?Q))

  (RULE (?Q)
    (OR ?P ?Q))

  (RULE ((NOT (OR ?P ?Q)))
    (NOT ?P))

  (RULE ((NOT (OR ?P ?Q)))
    (NOT ?Q))

  (RULE ((NOT ?P)
	 (NOT ?Q))
    (NOT (OR ?P ?Q)))

  (RULE ((NOT ?P)
	 (NOT ?Q))
    (NOT (OR ?Q ?P)))

  (rule (?P (not ?p))
    (false))

  (examine-rules))

(defun congruence-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (?w D)
    (= ((D D) B))
    (?f1 ((D) D))
    (?f2 ((D D) D)))


  (RULE NIL
    (= ?X ?X))

  (RULE ((= ?X ?Y))
    (= ?Y ?X))

  (RULE ((= ?X ?Y)
	 (= ?Y ?Z))
    (= ?X ?Z))

  (RULE ((= ?X ?Y))
    (= (?F1 ?X) (?F1 ?Y)))

  (RULE ((= ?X ?Y)
	 (= ?Z ?W))
    (= (?F2 ?X ?Z) (?F2 ?Y ?W)))
  
  (examine-rules))

(defun tax-test ()

  (system-init)

  (type-declarations
    (?C C)
    (?W C)
    (?Z C)
    (?r ((C) C))
    (fun ((((C) C)) B))
    (det ((C) B))
    (exst ((C) B))
    (is ((C C) B))
    (inter ((C C) B)))

  (rule ()
    (is ?c ?c))

  (rule ((is ?c ?w) (is ?w ?z))
    (is ?c ?z))

  (rule ((exst ?c) (det ?w) (is ?c ?w))
    (is ?w ?c))

  (rule ((is ?c ?w))
    (is (?r ?c) (?r ?w)))

  (rule ((exst ?c) (is ?c ?w))
    (exst ?w))

  (rule ((det ?w) (is ?c ?w))
    (det ?c))

  (rule ((fun ?r) (exst ?c))
    (exst (?r ?c)))

  (rule ((fun ?r) (det ?c))
    (det (?r ?c)))

  (rule ((exst (?r ?c)))
    (exst ?c))

  (rule ((exst ?c))
    (inter ?c ?c))

  (rule ((inter ?c ?w))
    (exst ?c))

  (rule ((inter ?c ?w) (is ?c ?z))
    (inter ?z ?w))

  (rule ((inter ?c ?w) (fun ?r))
    (inter (?r ?c) (?r ?w)))

  (rule ((inter ?c ?w))
    (inter ?w ?c))

  (rule ((inter ?c ?w) (det ?w))
    (is ?w ?c))

  (examine-rules))

(defun montague-test2 ()

  (system-init)

  (type-declarations
    (?x C)
    (?y C)
    (?w C)
    (every ((C) N))
    (some  ((C) N))
    (?R ((N) C))
    (is-every ((C C) B))
    (is-some  ((C C) B)))

  (RULE NIL
    (is-every ?x ?x))

  (RULE ((is-every ?X ?Y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (rule ((is-some ?x ?y))
    (is-some ?y ?x))

  (rule ((is-some ?x ?y))
    (is-some ?x ?x))

  (rule ((is-some ?x ?y)
	 (is-every ?y ?z))
    (is-some ?x ?z))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (some ?x)) (?R (some ?y))))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (every ?y)) (?R (every ?x))))

  (RULE ((is-some ?X ?Y))
    (is-every (?R (every ?x)) (?R (some ?y))))

  (examine-rules))

(defun montague-test3 ()

  (system-init)

  (type-declarations
    (?x C)
    (?y C)
    (?w C)
    (every ((C) N))
    (some  ((C) N))
    (?R ((N) C))
    (is-every ((C C) B))
    (is-some  ((C C) B)))

  (RULE NIL
    (is-every ?x ?x))

  (RULE ((is-every ?X ?Y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (rule ((is-some ?x ?y))
    (is-some ?x ?x))

  (rule ((is-some ?x ?y)
	 (is-every ?y ?z))
    (is-some ?x ?z))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (some ?x)) (?R (some ?y))))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (every ?y)) (?R (every ?x))))

  (RULE ((is-some ?X ?y)
	 (is-every ?x ?z))
    (is-every (?R (every ?z)) (?R (some ?y))))

  (examine-rules))

(defun montague-test4 ()

  (system-init)

  (type-declarations
    (not ((B) B))
    (or ((B B) B))
    (false (() B))

    (?x C)
    (?y C)
    (?z C)
    (?w C)
    (?p B)

    (thing (() C))
    (every ((C) ((C) B)))
    (some  ((C) ((C) B)))
    (?R ((((C) B)) C))
    (is ((((C) B)) C))
    (is-every ((C C) B))
    (is-some  ((C C) B))
    (determined ((C) B))
    (there-exists-a ((C) B))
    (not-there-exists-a ((C) B)))

  (rule (((every ?x) ?y))
    (is-every ?x ?y))

  (rule ((is-every ?x ?y))
    ((every ?x) ?y))

  (rule ((not (there-exists-a ?x)))
    (not-there-exists-a ?x))

  (rule ((not-there-exists-a ?x))
    (not (there-exists-a ?x)))

  (rule (?p
	  (not ?p))
    (false))

  (rule ((there-exists-a ?x)
	 (not-there-exists-a ?x))
    (false))

;the rules from the paper.

  (rule ()
    (there-exists-a (thing)))

  (rule ()
    (is-every ?x (thing)))

  (rule ((is-every ?x ?y))
    (is-every (?R (some ?x))
	      (?R (some ?y))))

  (rule ((is-every ?x ?y))
    (is-every (?R (every ?y))
	      (?R (every ?x))))

  (rule ((is-every ?x ?y)
	 (determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?y))
	      ?x))

  (rule ((is-every ?x ?y)
	 (determined ?y)
	 (there-exists-a ?y))
    (is-every ?y
	      (is (every ?x))))

  (rule ((is-every ?x ?y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (rule ()
    (is-every ?x ?x))

  (rule ((there-exists-a (?r (some ?x))))
    (there-exists-a ?x))

  (rule ((there-exists-a ?x)
	 (is-every ?x ?y))
    (there-exists-a ?y))

  (rule ((determined ?x)
	 (is-every ?y ?x))
    (determined ?y))

  (rule ((not (is-every ?x ?y)))
    (there-exists-a ?x))

  (rule ((there-exists-a ?x)
	 (determined ?y)
	 (is-every ?x ?y))
    (is-every ?y ?x))

  (rule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (?r (every ?y))
	      (?r (some ?z))))

  (rule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (is (every ?y)) ?z))

  (rule ((determined ?x)
	 (there-exists-a ?x))
    (is-every ?x (is (every ?x))))

  (rule ((determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?x)) ?x))

  (rule ((there-exists-a (is (every ?x)))
	 (there-exists-a ?x))
    (determined ?x))

  (rule ()
    (is-every ?x (is (some ?x))))

  (rule ()
    (is-every (is (some ?x)) ?x))

  (rule ((not-there-exists-a ?x))
    (is-every (thing) (?R (every ?x))))

  (rule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every (?r (some ?z))
	      (?r (every ?x))))

  (rule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every ?z (is (every ?x))))

  (rule ((not-there-exists-a ?y)
	 (is-every ?x ?y))
    (not-there-exists-a ?x))


    
  (examine-rules))

(defun montague-test5 ()

  (system-init)

  (contrapositive-type-declarations

    (?x C)
    (?y C)
    (?z C)
    (?w C)
    (?p B)

    (thing (() C))
    (every ((C) NP))
    (some  ((C) NP))
    (?R ((NP) C))
    (is ((NP) C))
    (is-every ((C C) B))
    (is-some  ((C C) B))
    (determined ((C) B))
    (there-exists-a ((C) B))
    (sen ((NP C) B)))

  (multirule ((sen (every ?x) ?y))
    (is-every ?x ?y))

  (multirule ((is-every ?x ?y))
    (sen (every ?x) ?y))

;the multirules from the paper.

  (multirule ()
    (there-exists-a (thing)))

  (multirule ()
    (is-every ?x (thing)))

  (multirule ((is-every ?x ?y))
    (is-every (?R (some ?x))
	      (?R (some ?y))))

  (multirule ((is-every ?x ?y))
    (is-every (?R (every ?y))
	      (?R (every ?x))))

  (multirule ((is-every ?x ?y)
	 (determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?y))
	      ?x))

  (multirule ((is-every ?x ?y)
	 (determined ?y)
	 (there-exists-a ?y))
    (is-every ?y
	      (is (every ?x))))

  (multirule ((is-every ?x ?y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (multirule ()
    (is-every ?x ?x))

  (multirule ((there-exists-a (?r (some ?x))))
    (there-exists-a ?x))

  (multirule ((there-exists-a ?x)
	 (is-every ?x ?y))
    (there-exists-a ?y))

  (multirule ((determined ?x)
	 (is-every ?y ?x))
    (determined ?y))

  (multirule ((not (is-every ?x ?y)))
    (there-exists-a ?x))

  (multirule ((there-exists-a ?x)
	 (determined ?y)
	 (is-every ?x ?y))
    (is-every ?y ?x))

  (multirule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (?r (every ?y))
	      (?r (some ?z))))

  (multirule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (is (every ?y)) ?z))

  (multirule ((determined ?x)
	 (there-exists-a ?x))
    (is-every ?x (is (every ?x))))

  (multirule ((determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?x)) ?x))

  (multirule ((there-exists-a (is (every ?x)))
	 (there-exists-a ?x))
    (determined ?x))

  (multirule ()
    (is-every ?x (is (some ?x))))

  (multirule ()
    (is-every (is (some ?x)) ?x))

  (multirule ((not (there-exists-a ?x)))
    (is-every (thing) (?R (every ?x))))

  (multirule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every (?r (some ?z))
	      (?r (every ?x))))

  (multirule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every ?z (is (every ?x))))
    
  (examine-rules))