ax.ss

gistfile1.txt

#lang racket
;;;;USAGE:
;Modify the lines following comments that begin with MODIFY:
;then run the program to get a proof

;;we use a recursive tree structure for formulas, so that a tree with left node A and right node B means A->B
(define-struct tree (left right not token) #:transparent)

;;create a tree by calling (mtree L R) where L and R are trees
(define (mtree l r)
  (make-tree l r #f null))

;;negate a tree by calling (Not T) where T is a tree
(define (Not t)
  (make-tree (tree-left t) (tree-right t) (not (tree-not t)) (tree-token t)))

;;create an atomic formula by calling (formula S) where S is a string
(define (formula s)
  (make-tree null null #f s))

;;EXMAPLE:
;;(mtree (mtree (formula "S") (Not (formula "T"))) (Not (mtree (formula "P") (formula "Q"))))
;;represents (S->~T)->~(P->Q)

;;MODIFY: this is what you're trying to prove. should be one tree
(define want (mtree (mtree (formula "p") (mtree (formula "q") (formula "r"))) (mtree (formula "q") (mtree (formula "p") (formula "r")))))

;;MODIFY: these are your hypotheses. should be a list of tree
(define hypotheses (list))

;;MODIFY: how many iterations should be done? Note - the code currently runs a factor slower than it should. Haven't figured out total complexity yet but definitely dependant on the complexity of provided formulas (size, and number of different variables)
(define maxiterations 1000)

;;Note - you can use this function to print out a tree to help you debug
(define (print-tree t)
  (when (tree-not t)
      (display "~"))
  (if (null? (tree-token t))
      ((lambda ()
         (print-tree-r (tree-left t))
         (display "->")
         (print-tree-r (tree-right t))))
      (display (tree-token t)))
  (display "  ")
  (void))

;;;;;;;;;;;;;;;;;;;;;;;;IMPLEMENTATION DETAILS BELOW THIS LINE;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (display-n . p)
  (for ((P p))
    (display P)))
  

(define (print-tree-r t)
  (when (tree-not t)
      (display "~"))
  (if (null? (tree-token t))
      ((lambda ()
         (display "(")
         (print-tree-r (tree-left t))
         (display "->")
         (print-tree-r (tree-right t))
         (display ")")))
      (display (tree-token t))))

(define (print-all t)
  (for ((T t))
    (print-tree T)))



(define (ax1 A B)
  (make-tree A (make-tree B A #f null) #f null))

(define origin-table (make-hash))

(define (make-ax1 lst)
  (define ret (list))
  (for ((A lst))
    (for ((B lst))
      (when (not (hash-has-key? origin-table (ax1 A B))) (hash-set! origin-table (ax1 A B) (list (list A B) 'ax1)))
      (set! ret (cons (ax1 A B) ret))))
  (remove-duplicates ret))

(define (ax2 A B C)
  (make-tree (make-tree A (make-tree B C #f null) #f null) (make-tree (make-tree A B #f null) (make-tree B C #f null) #f null) #f null))

(define (make-ax2 lst)
  (define ret (list))
  (for ((A lst))
    (for ((B lst))
      (for ((C lst))
        (when (not (hash-has-key? origin-table (ax2 A B C))) (hash-set! origin-table (ax2 A B C) (list (list A B C) 'ax2)))
      (set! ret (cons (ax2 A B C) ret)))))
  (remove-duplicates ret))

(define (ax3 A B)
  (mtree (mtree (Not A) B) (mtree (mtree (Not A) (Not B)) A)))


(define (make-ax3 lst)
  (define ret (list))
  (for ((A lst))
    (for ((B lst))
      (when (not (hash-has-key? origin-table (ax3 A B))) (hash-set! origin-table (ax3 A B) (list (list A B) 'ax3)))
      (set! ret (cons (ax3 A B) ret))))
  (remove-duplicates ret))


(define (all-subtrees t)
  (if (null? (tree-token t))
      (remove-duplicates (append (list t (Not t)) (all-subtrees (tree-left t)) (all-subtrees (tree-right t))))
      (list t (Not t))))

;;initially populate sequence with all information we can get from the hypotheses
(define sequence (remove-duplicates (append hypotheses (make-ax1 (append-map all-subtrees hypotheses)) (make-ax2 (append-map all-subtrees hypotheses)) (make-ax3 (append-map all-subtrees hypotheses)))))
(for ((f hypotheses))
  (hash-set! origin-table f (list (list f) 'hyp)))

(define have-recursed-on (make-hash))

(define (get-all-prereqs tail)
  (if (hash-has-key? have-recursed-on tail)
      (list)
      ((lambda ()
         (hash-set! have-recursed-on tail #t)
         (if (not (member tail sequence))
             (list)
             ((lambda ()
                (define newl (list))
                (for ((i (first (hash-ref origin-table tail))))
                  (when (member i sequence)
                    ((lambda ()
                       (set! newl (append newl (list i) (get-all-prereqs i)))))))
                (remove-duplicates (append (list tail) newl)))))))))

(define (final-seq)
  (define used (get-all-prereqs want))
  (define finalsequence (filter (lambda (x) (member x used)) sequence))
  (for ((f finalsequence) (line (build-list (length finalsequence) (curry + 1))))
    (define origin (second (hash-ref origin-table f)))
    (display-n "(" line ") ")
    (print-tree f)
    (cond
      [(equal? origin 'ax1)
       (display " by Ax1")]
      [(equal? origin 'ax2)
       (display " by Ax2")]
      [(equal? origin 'ax3)
       (display " by Ax3")]
      [(equal? origin 'hyp)
       (display " by hypothesis")]
      [(equal? origin 'inference)
       (display " by inference ")])
    (when (equal? origin 'inference)
        ((lambda ()
           (display-n "("
                      (+ 1 (- (length finalsequence) (length (member (first (first (hash-ref origin-table f))) finalsequence))))
                      ", "
                      (+ 1 (- (length finalsequence) (length (member (second (first (hash-ref origin-table f))) finalsequence))))
                      ")"))))
    (display "\n"))
  (void))
        
             
               

(define (done?)
  (if (not (false? (member want sequence)))
      (hash-ref origin-table want)
      #f))

;;appends all new formulas generated by the three axioms
(define (axioms!)
  (set! sequence (remove-duplicates (append sequence (make-ax1 (all-subtrees want)) (make-ax2 (all-subtrees want)) (make-ax3 (all-subtrees want))))))

;;appends all new formulas generated by inferences
(define (inferences!)
  (define new-sequence sequence)
  (for ((formula1 sequence))
    (for ((formula2 sequence))
      (when (equal? (tree-left formula1) formula2)
          ((lambda ()
             (when (not (hash-has-key? origin-table (tree-right formula1))) (hash-set! origin-table (tree-right formula1) (list (list formula1 formula2) 'inference)))
             (set! new-sequence (append new-sequence (list (tree-right formula1))))
             )))))
  (set! sequence (remove-duplicates new-sequence)))

(define iterations 0)
(define (attempt-to-solve max-iterations)
  (do ([i 0 (+ i 1)])
     ((or (= i max-iterations) (done?))
      ((lambda()
         (set! iterations i)
      (cond
       [(= i max-iterations) #f]
       [(done?) #t]))))
    (display-n "Iteration " i "...\n")
    (axioms!)
    (inferences!)))



((lambda ()
   (attempt-to-solve maxiterations)
   (if (done?)
    ((lambda ()
       (display-n "Found a proof in " iterations " iterations:\n")
       (final-seq)))
    ((lambda ()
       (display "Sorry! Couldn't find a proof. Try more iterations.\n"))))
   (void)))