;;;
;;; wff.lisp: Syntax of First-Order Logic
;;;
;;; By Philip W. L. Fong
;;;
;;; Defines the syntax of first-order terms and formulas (page 1-2,
;;; lecture 18). Also provides facilities for performing substitutions
;;; in a first-order formula (page 2, lecture 20).
;;;
;;; Example: The formula on page 7, lecture 20 is represented as
;;; follows:
;;;
;;; (forall ?x (and (p ?x ?x)
;;; (exists ?y (=> (forall ?x (p ?x ?y))
;;; (p ?x ?y)))))
;;;
;; Terms: constructors, selectors and recognizers
;; Variables
;; A variable is a symbol with its name beginning with '?'
;; e.g. '?a, '?this-is-a-variable, '?123
(defun make-fresh-variable ()
"Generate a fresh variable that is guaranteed to be different from
any existing variables."
(let ((v (gentemp "?")))
v))
(defun variable-p (term)
(and (symbolp term)
(eql #\? (char (symbol-name term) 0))))
;; Constants
;; A constant is a non-variable symbol.
;; e.g. 'a, 'this-is-a-constant
(defun constant-p (term)
(and (symbolp term)
(not (eql #\? (char (symbol-name term) 0)))))
;; Function applications
(defun make-funapp (symbol term-list)
(cons symbol term-list))
(defun funapp-symbol (funapp)
(first funapp))
(defun funapp-term-list (funapp)
(rest funapp))
(defun funapp-p (term)
(consp term))
;; WFF's: constructors, selectors and recognizers
;; Atomic formulas
(defun make-atom (predicate-sym term-list)
(cons predicate-sym term-list))
(defun atom-predicate-sym (atom)
(first atom))
(defun atom-term-list (atom)
(rest atom))
(defun atom-p (wff)
(not (member (first wff) '(not or and => <=> forall exists))))
;; Negations
(defun make-negation (wff)
(list 'not wff))
(defun negation-wff (negation)
(second negation))
(defun negation-p (wff)
(eq (first wff) 'not))
;; Disjunctions
(defun make-disjunction (wff1 wff2)
(list 'or wff1 wff2))
(defun disjunction-wff1 (disjunction)
(second disjunction))
(defun disjunction-wff2 (disjunction)
(third disjunction))
(defun disjunction-p (wff)
(eq (first wff) 'or))
;; Conjunctions
(defun make-conjunction (wff1 wff2)
(list 'and wff1 wff2))
(defun conjunction-wff1 (conjunction)
(second conjunction))
(defun conjunction-wff2 (conjunction)
(third conjunction))
(defun conjunction-p (wff)
(eq (first wff) 'and))
;; Implications
(defun make-implication (wff1 wff2)
(list '=> wff1 wff2))
(defun implication-wff1 (implication)
(second implication))
(defun implication-wff2 (implication)
(third implication))
(defun implication-p (wff)
(eq (first wff) '=>))
;; Equivalences
(defun make-equivalence (wff1 wff2)
(list '<=> wff1 wff2))
(defun equivalence-wff1 (equivalence)
(second equivalence))
(defun equivalence-wff2 (equivalence)
(third equivalence))
(defun equivalence-p (wff)
(eq (first wff) '<=>))
;; Universally quantified formulas
(defun make-universal (var wff)
(list 'forall var wff))
(defun universal-var (universal)
(second universal))
(defun universal-wff (universal)
(third universal))
(defun universal-p (wff)
(eq (first wff) 'forall))
;; Existentially quantified formulas
(defun make-existential (var wff)
(list 'exists var wff))
(defun existential-var (existential)
(second existential))
(defun existential-wff (existential)
(third existential))
(defun existential-p (wff)
(eq (first wff) 'exists))
;;
;; Substitution mechanism for WFF and terms.
;; An implementation of the algorithm specified in page 2 of lecture 20.
;;
(defun wff-substitute (wff var value)
"Substitue a term VALUE for a free variable VAR in a formula WFF."
(cond
((negation-p wff)
(make-negation (wff-substitute (negation-wff wff) var value)))
((disjunction-p wff)
(make-disjunction (wff-substitute (disjunction-wff1 wff) var value)
(wff-substitute (disjunction-wff2 wff) var value)))
((conjunction-p wff)
(make-conjunction (wff-substitute (conjunction-wff1 wff) var value)
(wff-substitute (conjunction-wff2 wff) var value)))
((implication-p wff)
(make-implication (wff-substitute (implication-wff1 wff) var value)
(wff-substitute (implication-wff2 wff) var value)))
((equivalence-p wff)
(make-equivalence (wff-substitute (equivalence-wff1 wff) var value)
(wff-substitute (equivalence-wff2 wff) var value)))
((universal-p wff)
(if (eq (universal-var wff) var)
wff
(make-universal (universal-var wff)
(wff-substitute (universal-wff wff) var value))))
((existential-p wff)
(if (eq (existential-var wff) var)
wff
(make-existential (existential-var wff)
(wff-substitute (existential-wff wff) var value))))
(t (atom-substitute wff var value))))
(defun atom-substitute (atom var value)
"Substitute a term VALUE for free variable VAR in an atomic formula ATOM."
(make-atom (atom-predicate-sym atom)
(mapcar #'(lambda (x) (term-substitute x var value))
(atom-term-list atom))))
(defun term-substitute (term var value)
"Substituting a term VALUE for free variable VAR in a term TERM."
(cond
((constant-p term) term)
((variable-p term)
(if (eq term var)
value
term))
(t
(make-funapp (funapp-symbol term)
(mapcar #'(lambda (x) (term-substitute x var value))
(funapp-term-list term))))))