; Regarding the algorithm in the text:  note that after step 4
;   scope information has been lost.  This may result in
;   extra arguments to Skolem functions.  This isn't wrong, really, but
;   just awkward.  If you want, you may swap steps 4  & 5, although you
;   needn't. 


(define d1 '((forall ?x) (implies (implies (p ?x) (q ?x)) (r ?x))))
(define d2 '((forall ?x) (implies (p ?x) (implies (q ?x) (r ?x)))))
(define d3 '(or ((forall ?x) (male ?x)) ((forall ?x) (female ?x))))
(define d4 '((forall ?z) (not ((forall ?y) (implies (p ?y ?z) (q ?y ?z))))))
(define d5 '(implies ((forall ?x) (implies (not (p ?x)) (not (q ?x))))
                     ((forall ?x) (implies (p ?x) (q ?x)))))
(define d6 '(and ((forall ?x) (implies (p ?x) ((exists ?y) (q ?x ?y))))
                 ((forall ?x) (implies ((exists ?y) (q ?x ?y)) (p ?x)))))
(define d7 '(or (not ((forall ?x) (implies (p ?x) ((exists ?y) (q ?x ?y)))))
                (not ((forall ?x) (implies ((exists ?y) (q ?x ?y)) (p ?x))))))
(define d8 '((forall ?a)
             ((forall ?b)
              ((forall ?c)
               (not ((forall ?d) (implies (p ?a ?b) (or (q ?c) (r ?d)))))))))
(define d9 '((exists ?a) 
             ((forall ?b) 
              ((exists ?c) 
               ((forall ?d) 
                ((exists ?e)
                 (and (and (p ?a ?b) (q ?c ?d)) (r ?e f))))))))



; The input is assumed to conform to the following grammar:

; Sentence -> QuantifiedSentence | CompoundSentence | PrimitiveSentence
; QuantifiedSentence -> ( Quantifier Sentence )
; Quantifier -> ( forall Variable ) | ( exists Variable )
; CompoundSentence -> ( not Sentence ) ( and Sentence Sentence ) |
;                     ( or Sentence Sentence ) ( implies Sentence Sentence )
; PrimitiveSentence -> ( PredicateName Terms )
; Terms ->  Term | Term Terms
; Term  ->  Variable | ObjectConstant


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; TYPES ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Four types are assumed:  QUANTIFIED-SENTENCE (with subtypes EXISTENTIAL
;   and UNIVERSAL), NEGATED-SENTENCE, COMPOUND-SENTENCE (with subtypes
;   DISJUNCTION, CONJUNCTION, and IMPLICATION; note that NEGATED-SENTENCE,
;   being unary, is not considered a subtype), and ATOM


;;;;;;;;;;;;;;;;;;;; SELECTORS AND CONSTRUCTORS ;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;; for QUANTIFIED-SENTENCES ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Quantified sentences consist of a QUANTIFIER (itself consisting of
;   a QUANTIFIER-TYPE and a VARIABLE) and a QUANTIFIED sentence
; No type checking is done on the arguments to the selectors

(define (quantifier s) (car s))
(define (quantified s) (cadr s))
(define (quantifier-type s) (caar s))

(define (variable s) (cadar s))
(define (build-quantifier qt v) (list qt v))
(define (build-quantified q s) (list q s))

(define (quantified-sentence? s)
  (and (pair? s) (pair? (car s)) (member (caar s) '(forall exists))))
(define (existential? s)
  (and (quantified-sentence? s) (eq? (car (quantifier s)) 'exists)))


;;;;;;;;;;;;;;;;;;;; for COMPOUND-SENTENCES ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Compound sentences consist of a connective (AND, OR, or IMPLIES)
;   and two arguments ARG1 and ARG2, which are sentences

(define (connective s) (car s))
(define (arg1 s) (cadr s))
(define (arg2 s) (caddr s))

(define (build-compound c a1 a2) (list c a1 a2))

(define (compound-sentence? s)
  (and (pair? s) (member (car s) '(and or implies))))
(define (implication? s)
  (and (compound-sentence? s) (eq? (connective s) 'implies)))
(define (conjunction? s)
  (and (compound-sentence? s) (eq? (connective s) 'and)))
(define (disjunction? s)
  (and (compound-sentence? s) (eq? (connective s) 'or)))


;;;;;;;;;;;;;;;;;;;;;;;;; for NEGATIONS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Negations have an argument ARG, which is a sentence, and a
;   CONNECTIVE, which always has value NOT and is used only
;   by the predicate NEGATION? (and already has the proper definition)
; Rather than a constructor, an operator NEGATE is provided that
;   removes a negation if one is already present, and adds one if not

(define (arg s) (cadr s))

(define (negation? s)
  (and (pair? s) (eq? (connective s) 'not)))

(define (negate s)
  (if (negation? s)
      (arg s)
      (list 'not s)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;; for ATOMS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; ATOMS consist of a RELATION-NAME and an ARG-LIST of terms
; No predicate is given for testing atomhood; it is assumed that
;  a sentence that is not a negation, a compound sentence, or a
;  quantified sentence is an atom
; This type may also be used for Skolem functions.

(define (relation-name s) (car s))
(define (arg-list s) (cdr s))

(define (build-atom r a) (cons r a))