;;; -*- Mode:Lisp; Package: User; Syntax:Common-Lisp; Base:10;-*-
;;; ************************************************************************
;;; FLAIR PROJECT
;;; ************************************************************************
;;; Filename: clausal-alg.cl
;;; ========================================================================
;;; CLAUSIFICATION ALGORITHM
;;; It is derived from Genesereth+Nilsson: Logical Foundations of Artificial
;;; Intelligence, pp63-66
;;; Code to put a prefix formula, possibly with quantifiers, etc.
;;; into clausal form, i.e. as a list of clauses, where each clause is a
;;; list of literals [an atom or its negation].
;;; NOTE: The given formula must be grammatically correct. It may contain
;;; free variables, in which case they will be assumed to be universally
;;; quantified.
;;; THE LANGUAGE:
;;; Variables are symbols starting with a question mark, for example ?x21.
;;; The logical connectives are:
;;; ~ (not)
;;; & (and)
;;; or
;;; => (if .. then)
;;; <=> (iff)
;;; The quantifiers are:
;;; ALL
;;; EXIST
;;; An example of conversion is from:
;;; (all ?x (exist ?y (<=> (p ?x a) (q a ?y))))
;;; to:
;;; (((~ (p ?x198)) (q a (skolem197 ?x198)))
;;; ((~ (q a (skolem197 ?x199))) (p ?x199 a)))
;;; NOTE: This code can be used as is (no additional code is required).
;;;--------------------------------------------------------------------
(defun convert-to-clause-form (expr)
;; Converts expr to clause form
;; Inputs: The expression expr
;; Outputs: A list of clauses obtained from expr.
;; NOTE: This function could have been written as a single assignment.
;; It has been written as a sequence of assignments to stress the
;; successive transformations.
(setq expr (unbound-to-universal expr)) ; It universally quantifies all the
; variables that are not bound in expr
(setq expr (eliminate-implies expr)) ; Eliminate => and <=>
(setq expr (reduce-scope-of-not expr)) ; The scope of ~ is an atom
(setq expr (unique-quant-variables expr)) ; Make sure all quantified
; variables are distinct
(setq expr (eliminate-existentials expr)) ; Use Skolem functions to
; eliminate existential quantifiers
(setq expr (eliminate-universals expr)) ; Eliminate universal quantifiers
(setq expr (distributive expr)) ; Do not leave & within scope of or
(setq expr (form-clauses expr)) ; Create clauses
(setq expr (standardize-apart expr))) ; Make sure that distinct clauses do
; not share variables
(defun unbound-to-universal (expr)
;; expr is a formula where some variables may be unbound.
;; Universally bound them.
;;REMINDER: 'labels' is a way of declaring local functions.
(labels ((find-unbound (e &optional bound &aux unbound)
;; Returns the variables that occur in e and are not in bound
(cond ((varp e) (unless (member e bound)
(list e)))
((atom e) nil)
((member (first e) '(all exist))
(setq bound (cons (second e) bound))
(find-unbound (third e) bound))
(t
(dolist (a (rest e))
(setq unbound (append (find-unbound a bound) unbound)))
unbound))))
(dolist (v (find-unbound expr))
(setq expr (list 'all v expr))))
expr)
(defun eliminate-implies (e &aux f1 f2)
;; Eliminates implications => and <=> from the input expression e
(cond ((atom e)
e)
((eq (first e) '=>)
(list 'or (list '~ (eliminate-implies (second e)))
(eliminate-implies (third e))))
((eq (first e) '<=>)
(setq f1 (eliminate-implies (second e)))
(setq f2 (eliminate-implies (third e)))
(list '&
(list 'or (list '~ f1) f2)
(list 'or (list '~ f2) f1)))
(t (mapcar #'eliminate-implies e))))
(defun reduce-scope-of-not (e &aux f1)
;; Reduces the scope of not in form e to a single atomic formula
(cond ((atom e)
e)
((not (eq (first e) '~))
(mapcar #'reduce-scope-of-not e))
(t ;; e starts with ~
(setq f1 (second e))
(cond ((atom f1)
e)
((eq (first f1) '~)
(reduce-scope-of-not (second f1)))
((eq (first f1) 'or)
(list '& (reduce-scope-of-not (list '~ (second f1)))
(reduce-scope-of-not (list '~ (third f1)))))
((eq (first f1) '&)
(list 'or (reduce-scope-of-not (list '~ (second f1)))
(reduce-scope-of-not (list '~ (third f1)))))
((eq (first f1) 'all)
(list 'exist (second f1) (reduce-scope-of-not (list '~ (third f1)))))
((eq (first f1) 'exist)
(list 'all (second f1) (reduce-scope-of-not (list '~ (third f1)))))
(t
e)))))
(defun unique-quant-variables (e)
;; It makes sure that in e each quantifier operates on a distinct variable
(cond ((atom e)
e)
((member (first e) '(all exist))
(cons (first e) (subst (new-var) (second e)
(unique-quant-variables (rest e)))))
(t
(mapcar #'unique-quant-variables e))))
(defun eliminate-existentials (e &optional vars)
;; Eliminates existential quantifiers from e. Then each occurrence of the
;; existentially quantified variable y which is dependent on the
;; universal variables vars x1 x2 .. is replaced by a term of the form
;; (SKOLEM x1 x2 ..)
(labels ((make-skolem-func (uargs)
;; Returns a Skolem function of uargs or a constant if no arguments
(if (null uargs)
(gentemp "SKOLEM")
(cons (gentemp "SKOLEM") uargs))))
(cond ((atom e)
e)
((eq (first e) 'all)
(list (first e) (second e)
(eliminate-existentials (third e) (cons (second e) vars))))
((eq (first e) 'exist)
(subst (make-skolem-func (reverse vars))
(second e) (eliminate-existentials (third e) vars)))
(t
(mapcar #'(lambda (f) (eliminate-existentials f vars)) e)))))
(defun eliminate-universals (e)
;; It returns m where m is obtained by eliminating the
;; universal quantifiers in e.
(cond ((atom e)
e)
((eq (first e) 'all)
(eliminate-universals (third e)))
(t
(mapcar #'eliminate-universals e))))
(defun distributive (e &aux l r)
;; Applies distributivity to all forms like
;; (or a (& b c)) or like (or (& a b) c)
;; i.e. we get conjunctions of disjuncts, a conjunctive form.
;; After this transformation no & will be within the scope of an or.
(cond ((atom e)
e)
((eq (first e) '~)
e) ;; e is an atom
((eq (first e) '&)
(list '& (distributive (second e)) (distributive (third e))))
((eq (first e) 'or)
(setq l (distributive (second e)))
(setq r (distributive (third e)))
(cond ((and (consp l) (eq (first l) '&))
(list '& (distributive (list 'or (second l) r))
(distributive (list 'or (third l) r))))
((and (consp r) (eq (first r) '&))
(list '& (distributive (list 'or l (second r)))
(distributive (list 'or l (third r)))))
(t
(list 'or l r))))
(t e))) ;; e is an atom
(defun form-clauses (e)
;; e is in conjunctive form. Eliminate all & and or and return a list
;; of lists of literals.
(labels ((squash-and (f) ;; if f starts with &, it returns a list
;; of its conjuncts; otherwise it returns (f)
(if (and (consp f) (eq (first f) '&))
(append (squash-and (second f)) (squash-and (third f)))
(list (squash-or f))))
(squash-or (f) ;; if f starts with or, it returns a list
;; of its disjuncts; otherwise it returns (f)
(if (and (consp f) (eq (first f) 'or))
(append (squash-or (second f)) (squash-or (third f)))
(list f))))
(squash-and e)))
(defun standardize-apart (e)
;; It makes sure that distinct clauses use distinct variables.
(labels ((find-variables (e)
;; Returns as a list all the variables in e
(cond ((varp e) (list e))
((atom e) nil)
(t
(remove-duplicates
(append (find-variables (first e))
(find-variables (rest e))))))))
(mapcar #'(lambda (c)
(dolist (v (find-variables c))
(setq c (subst (new-var) v c)))
c)
e)))
(defun varp (x)
;; To check to see if something is a variable, just check to see if the
;; first character is a "?".
;; For example, (varp '?A) => T, (varp "Ann") => nil.
(and (symbolp x)
(char= (char (symbol-name x) 0) '#\?)))
(defun new-var ()
;; It returns a new variable symbol.
(gentemp "?X"))