;;; This function converts a formula with explicit quantification into one
;;; with implicit quantification.  It performs both standardization (renaming
;;; of variables to insure uniqueness) and skolemization.  There is no sanity
;;; checking whatsoever; the original formula is assumed to be well-formed.

(defun skolemize (formula)
  (skolem-aux formula nil nil nil))

;;; This does the real work.  Its arguments are:
;;;   form   -  the formula being converted
;;;   parity -  keeps track of how many negations ("not" or "if"
;;;             antecedents) the current form is embedded inside
;;;             (nil <--> even, t <--> odd)
;;;   u-vars -  an association list of pairs
;;;             (original symbol . newly generated symbol)
;;;             for variables that are actually universally
;;;             quantified and inside whose scope of definition the
;;;             current form lies
;;;   e-vars -  an association list of pairs
;;;             (original symbol . skolem form)
;;;             for variables that are actually existentially quantified

(defun skolem-aux (form parity u-vars e-vars)
  (cond ((null form) nil)

	((atom form)
	 (or (u-variable form u-vars) ; replace univ. quant. variable
	     (sk-form form e-vars)    ; replace exist. quant. variable
	     form))                   ; leave anything else as is

	;; "not" form case
	((eql (first form) 'not)
	 (cons 'not
	       (skolem-aux (rest form) (not parity) u-vars e-vars)))

	;; "if" form case
	((eql (first form) 'if)
	 (list 'if
	       (skolem-aux (second form) (not parity) u-vars e-vars)
	       (skolem-aux (third form) parity u-vars e-vars)))

	;; existential quantifier case
	((or (and (eql (first form) 'forall) parity)
	     (and (eql (first form) 'exists) (not parity)))
	 (skolem-aux (third form) parity
		     u-vars (add-e-vars (second form) u-vars e-vars)))

	;; universal quantifier case
	((or (and (eql (first form) 'forall) (not parity))
	     (and (eql (first form) 'exists) parity))
	 (skolem-aux (third form) parity
		     (add-u-vars (second form) u-vars) e-vars))

	(t (cons (skolem-aux (first form) parity u-vars e-vars)
		 (skolem-aux (rest form) parity u-vars e-vars)))
	))

;;; This returns the new name for a universally quantified variable
;;; if there is one in the association list and nil otherwise.

(defun u-variable (symbol u-vars)
  (rest (assoc symbol u-vars)))

;;; This returns the skolem function form for an existentially
;;; quantified variable stored in the association list and nil
;;; otherwise.

(defun sk-form (symbol e-vars)
  (rest (assoc symbol e-vars)))

;;; This returns a new association list for existential variables which stores
;;; for each variable its skolem function form, which has as arguments all
;;; universal variables inside whose scope of definition these new existential
;;; variables are defined.

(defun add-e-vars (new-e-vars u-vars e-vars)
  (append (mapcar
	   #'(lambda (var)
	       (cons var (cons (new-sk-symbol var)
				(mapcar #'rest u-vars))))
	   new-e-vars)
	  e-vars))

;;; This returns a new association list for universal variables
;;; which stores their new names.

(defun add-u-vars (new-u-vars u-vars)
  (append (mapcar #'(lambda (var) (cons var (new-u-symbol var)))
		  new-u-vars)
	  u-vars))

;;; These functions return newly generated symbols for skolem functions and
;;; universally quantified variables.  Note that if standardization were not
;;; necessary, we'd get a better looking output if new-u-symbol did not include
;;; the gensym.  For either function, concatenating in the original variable
;;; name is done purely to make it easier for someone looking at the input and
;;; output to relate variables in the two expressions, and also to preserve
;;; some of the mnemonic information if the original variable names were chosen
;;; to have some mnemonic content.

(defun new-sk-symbol (var)
  (gensym (concatenate 'string "sk-" (string var) "-")))

(defun new-u-symbol (var)
  (gensym (concatenate 'string "?" (string var) "-")))

;;;;;;;;;;;;;;;;;;;;;;;;;;;; Some test data ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(setq testform1
      '(forall (x y) (not (exists (z)
				  (if (f y x) (or (g x z) (g y z)))))))

(setq testform2
      '(forall (x y) (exists (z)
			     (if (f y x) (or (g x z) (g y z))))))

(setq testform3
      '(and (forall (x y) (exists (z) (f x z)))
	    (forall (x) (or (p x a b)
			    (exists (y) (g y x))))
	    (forall (z) (not (exists (x) (h z x))))))

;;; To see what skolemize does to these, with the output formatted
;;; reasonably, type, for example
;;; (pprint testform1)
;;; (pprint (skolemize testform1))