Solution of Ertan DENIZ

;CENG Homework 3
;Ertan Deniz
;1250216


;Function "intersection?" that looks if there is any formula occuring on both
;sides of the sequent arrow.
(define (intersection? left right)
    (cond ((and (empty? Left)
  	        (empty? right)) #f)
          ((empty? left) #f)
          ((empty? right) #f)
          ((list? (first left)) (if (equal? (first left) (first right))
                                    #t
                                    (intersection? left (bf right))))
          ((member? (first left) right) #t)
          (else (intersection? (bf left) right))
     )
);=====>>> End of "intersection?" function.


;Function "R5" that determines any implication arrows and eliminates them 
;according to wang's algorithm. R5 takes only one argument, so it have to 
;be applied seperately over the two sides of the sequent arrow.
(define (R5 any-list)
     (if (equal? any-list '())
         any-list
         (if (equal? (first (first any-list)) '>)
             (cons (list 'or
                          (list 'not (second (first any-list)))
                          (last (first any-list)))
                   (R5 (bf any-list)))
             (cons (first any-list) (R5 (bf any-list)))
         )
     )
) ;====>>>End of "R5" function.

;Function "R1" takes two arguments, then copies the formulas in the first
;argument starting with "not" to the second argument. 
(define (R1 list1 list2)
      (if (empty? list1)
          list2
          (if (list? (first list1))
              (if (member? 'not (first list1))
                  (append (bf (first list1)) (R1 (bf list1) list2))
                  (R1 (bf list1) list2)
	        )
              (R1 (bf list1) list2)
	    )
	)
);====>>>End of "R1" function.


;Function "remaining-list" takes one argument and eliminates all the top level
;formulas starting with "not".
(define (remaining-list liste)
     (append (keep word?
                   liste)
             (keep (lambda (x) (not (member? 'not x)))
                   (keep list? liste)))
);===>>> End of "remaining-list".

;Function "AND-OR" that applies the rules of wang's algorithm for "AND on the left" 
;and "OR on the right". AND-OR takes two arguments, the first one should be "and" or "or"
;and the second one should be the left side of the sequent arrow for "and", and the right 
;side for "or".
(define (AND-OR Z a-list)
     (if (empty? a-list)
         a-list
         (if (equal? Z (first (first a-list)))
             (append (bf (first a-list))
                     (AND-OR Z (bf a-list)))
             (cons (first a-list)
                   (AND-OR Z (bf a-list))
		 )
         )
      )
);End of "AND-OR".

;=======>>>>Examples of calling "AND-OR" function
;   (and-or 'and left) ; don't write right instead of left!!!!
;   (and-or 'or right) ; don't write left instead of right!!!
;=======>>>>


;Function "AND-OR-2" applies the rule of "And on the right" and "OR on the left".
;Takes two arguments. First one is either "and" or "or, the second one is an appropriate
;list for "and" or "or".
(define (AND-OR-2 W list1)
      (if (empty? list1)
           list1
           (if (equal? (first (first list1)) W)
               (helper (bf (first list1)) (bf list1))
               (AND-OR-2 W (append (bf list1) (list (first list1))))
           )
      )
);End of "AND-OR-2".

;===============>>>>> Helper for AND-OR-2!!!
   (define (helper list1 list2)
   (if (empty? list1)
       '()
       (cons (cons (first list1) list2) (helper (bf list1) list2))))
;=================>>>>>>>>>>>END of Helper!!!!




;"test" function takes two arguments, the first one is a connective and the second 
;one a list. "test" gives #t if the given connective is in one of the top level formulas
;in the list. Else it gives #f.
(define (test D set)
    (if (empty? set)
        #f
        (if (list? (first set))
            (if (equal? (first (first set)) D)
                #t
                (test D (bf set)))
            (test D (bf set)))))


;"wang" function applies the rules of wang over the left or right lists and then
;calls wang recursively.If there are no connectives and there cannot be applied any
;rule of wang's algorithm over the two sides of the sequent arrow then "wang" returns #f.

      (define (wang left right)
         (cond
            ;Test for axiom:
               ((intersection? left right) #t)

            ;Eliminate the implication connectives if there are any
               ((or (test '> left)
                    (test '> right)) (wang (R5 left) (R5 right)))

            ;NOT on the right or NOT on the left:
               ((or (test 'not right)
                    (test 'not left))  (wang (R1 right (remaining-list left))
                      			     (R1 left (remaining-list right))))
            ;OR on the right or AND on the left:
               ((or (test 'or right)
                   (test 'and left)) (wang (and-or 'and left) (and-or 'or right)))

            ;OR on the left:
               ((test 'or left) (for-all? (and-or-2 'or left) (lambda (x) (wang x right))))

            ;AND on the right:
               ((test 'and right) (for-all? (and-or-2 'and right) (lambda (y) (wang left y))))

               (else #f)

         )
      );====>>>End of "wang".