gistfile1.el

(defun mp (s1 s2)
  (when (and (listp s1)
             (equal '⊃ (elt s1 0))
             (equal s2 (elt s1 1)))
    (elt s1 2)))

(defun mt (s1 s2)
  (when (and (listp s1)
             (equal '⊃ (elt s1 0))
             (listp s2)
             (equal '¬ (elt s2 0))
             (equal (elt s1 2)
                    (elt s2 1)))
    (list '¬ (elt s1 1))))

(defun hs (s1 s2)
  (when (and (listp s1)
             (listp s2)
             (equal '⊃ (elt s1 0))
             (equal '⊃ (elt s2 0))
             (equal (elt s1 2) (elt s2 1)))
    (list '⊃ (elt s1 1) (elt s2 2))))

(defun ds (s1 s2)
  (when (and (listp s1)
             (listp s2)
             (equal '∨ (elt s1 0))
             (equal '¬ (elt s2 0))
             (equal (elt s1 1) (elt s1 1)))
    (elt s1 2)))

(defun wastep (target history)
  (let ((ta (make-hash-table :test 'equal)))
    (progn
      (dolist (h history)
        (let* ((result (elt h 2)))
          (puthash result 0 ta)))
      (puthash target 1 ta)
      (dolist (h history)
        (dolist (i (cdr (elt h 1)))
          (let ((v (or (gethash i ta) 0)))
            (puthash i (+ v 1) ta))))
      (let ((r nil))
        (maphash (lambda (k v)
                   (when (zerop v)
                     (setq r 't)))
                 ta)
        r))))

(defun proof-stream (x prepositions history)
  (if (member x prepositions)
      (when (not (wastep x history))
        (list (vector (reverse history))))
    (mapcar
     (lambda (statement1)
       (mapcar
        (lambda (statement2)
          (mapcar
           (lambda (rule)
             (vector :call rule statement1 statement2 history prepositions x))
           '(mp mt hs ds)))
        prepositions))
     prepositions)))

(defun run (n x)
  (let ((results nil))
    (progn
      (while (> n (length results))
        (cond
         ((null x) (setq n 0))
         ((listp (car x))
          (setq x (append (car x) (cdr x))))
         ((and (vectorp (car x))
               (equal :call (aref (car x) 0)))
          (let* ((v (car x))
                 (rule (aref v 1))
                 (s1 (aref v 2))
                 (s2 (aref v 3))
                 (h (aref v 4))
                 (p (aref v 5))
                 (target (aref v 6))
                 (y (funcall rule s1 s2)))
            (progn
              (setq x (cdr x))
              (when (and y (not (member y p)))
                (let ((sfr (proof-stream
                            target
                            (cons y p)
                            (cons `(⊃ (,rule ,s1 ,s2) ,y) h))))
                  (setq x (cons sfr x)))))))
         (:else (progn
                  (when (not (member (aref (car x) 0) results))
                    (setq results (cons (aref (car x) 0) results)))
                  (setq x (cdr x))))))
      (reverse results))))

(defun prove (n target preps)
  (run n (proof-stream target preps nil)))

(defun display-proofs (sols)
  (with-output-to-string
    (princ "\n(results\n ")
    (dotimes (i (length sols))
      (when (> i 0)
        (princ " "))
      (princ "(")
      (princ 'proof)
      (princ " ")
      (princ i)
      (princ ")")
      (princ "\n")
      (dolist (ii (elt sols i))
        (princ " ")
        (princ ii)
        (princ "\n")))
    (princ " )\n")))

(insert
 (display-proofs
  (prove 100
         '(¬ P)
         '((⊃ (≡ L N) C)
           (∨ (≡ L N) (⊃ P (¬ E)))
           (⊃ (¬ E) C)
           (¬ C)))))
(results
 (proof 0)
 (⊃ (mt (⊃ (≡ L N) C) (¬ C)) (¬ (≡ L N)))
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (≡ L N))) (⊃ P (¬ E)))
 (⊃ (hs (⊃ P (¬ E)) (⊃ (¬ E) C)) (⊃ P C))
 (⊃ (mt (⊃ P C) (¬ C)) (¬ P))
 (proof 1)
 (⊃ (mt (⊃ (≡ L N) C) (¬ C)) (¬ (≡ L N)))
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (≡ L N))) (⊃ P (¬ E)))
 (⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
 (⊃ (mt (⊃ P (¬ E)) (¬ (¬ E))) (¬ P))
 (proof 2)
 (⊃ (mt (⊃ (≡ L N) C) (¬ C)) (¬ (≡ L N)))
 (⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (≡ L N))) (⊃ P (¬ E)))
 (⊃ (mt (⊃ P (¬ E)) (¬ (¬ E))) (¬ P))
 (proof 3)
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ C)) (⊃ P (¬ E)))
 (⊃ (hs (⊃ P (¬ E)) (⊃ (¬ E) C)) (⊃ P C))
 (⊃ (mt (⊃ P C) (¬ C)) (¬ P))
 (proof 4)
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ C)) (⊃ P (¬ E)))
 (⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
 (⊃ (mt (⊃ P (¬ E)) (¬ (¬ E))) (¬ P))
 (proof 5)
 (⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
 (⊃ (mt (⊃ (≡ L N) C) (¬ C)) (¬ (≡ L N)))
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (≡ L N))) (⊃ P (¬ E)))
 (⊃ (mt (⊃ P (¬ E)) (¬ (¬ E))) (¬ P))
 (proof 6)
 (⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (¬ E))) (⊃ P (¬ E)))
 (⊃ (mt (⊃ P (¬ E)) (¬ (¬ E))) (¬ P))
 (proof 7)
 (⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (¬ E))) (⊃ P (¬ E)))
 (⊃ (hs (⊃ P (¬ E)) (⊃ (¬ E) C)) (⊃ P C))
 (⊃ (mt (⊃ P C) (¬ C)) (¬ P))
 (proof 8)
 (⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
 (⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ C)) (⊃ P (¬ E)))
 (⊃ (mt (⊃ P (¬ E)) (¬ (¬ E))) (¬ P))
 )







;; (display-proofs
;;  (prove 2
;;         '(¬ K) 
;;         '((⊃ K T)
;;           (¬ T))))

;; (display-proofs
;;  (prove
;;   5
;;   '(¬ B)
;;   '((⊃ (¬ A) (⊃ B (¬ C)))
;;     (⊃ (¬ D) (⊃ (¬ C) A))
;;     (∨ D (¬ A))
;;     (¬ D))))