sat.scm

(define (tautology? p #!optional arity)
  (contradiction? (compose N p)
    (procedure-arity/default p arity)))

(define valid? tautology?)

(define (contradiction? p #!optional arity)
  (not (satisfiable? p
         (procedure-arity/default p arity))))

(define unsatisfiable? contradiction?)

(define (contingent? p #!optional arity)
  (let ((arity (procedure-arity/default p arity)))
    (and (not (tautology? p arity))
         (not (contradiction? p arity)))))

(define (satisfiable? p #!optional arity)
  (any (lambda (interpretation)
         (= (apply p interpretation) 1))
       (cartesian-power
         '(0 1)
         (procedure-arity/default p arity))))

(define (invalid? p #!optional arity)
  (not (tautology? p
         (procedure-arity/default p arity))))

(define (equivalent? p q #!optional arity)
  (tautology? (compose E p q)
    (max (procedure-arity/default p arity)
         (procedure-arity/default q arity))))

(define ((compose p . formulas) . interpretations)
  (apply p
         (map (lambda (q) (apply q interpretations))
              formulas)))

(define (procedure-arity/default p arity)
  (if (not (default-object? arity))
    arity
    (procedure-arity-min (procedure-arity p))))

(define (cartesian-power A n)
  (if (= n 0)
    '(())
    (cartesian-product A (cartesian-power A (- n 1)))))

(define (cartesian-product A B)
  (append-map
    (lambda (x)
      (map (lambda (y)
             (append
               (if (list? x) x (list x))
               (if (list? y) y (list y))))
           B))
    A))

(define (N p)
  (cond ((= p 0) 1)
        ((= p 1) 0)))

(define (K p q)
  (cond ((and (= p 0) (= q 0)) 0)
        ((and (= p 0) (= q 1)) 0)
        ((and (= p 1) (= q 0)) 0)
        ((and (= p 1) (= q 1)) 1)))

(define (A p q) (N (K (N p) (N q))))

(define (C p q) (A (N p) q))

(define (E p q) (K (C p q) (C q p)))

(for-each
  (lambda (p) (display (tautology? p)) (newline))
  (list
    ; modus ponens
    (lambda (p q) (C (K (C p q) p) q))
    ; affirmatio consequentis
    (lambda (p q) (C (K (C p q) q) p))
    ; negatio antecedentis
    (lambda (p q) (C (K (C p q) (N p)) (N q)))
    ; modus tollens
    (lambda (p q) (C (K (C p q) (N q)) (N p)))
    ; syllogismus hypotheticus
    (lambda (p q r) (C (K (C p q) (C q r)) (C p r)))
    ; De Morgan's laws
    (lambda (p q) (E (N (K p q)) (A (N p) (N q))))
    (lambda (p q) (E (N (A p q)) (K (N p) (N q))))
    ; Peirce's law
    (lambda (p q) (C (C (C p q) p) p))
    ; reductio ad absurdum
    (lambda (p) (C (C p (N p)) (N p)))
    ; consequentia mirabilis
    (lambda (p) (C (C (N p) p) p))
    ; proof by contradiction
    (lambda (p q) (C (C p (K q (N q))) (N p)))
    ; indirect proof
    (lambda (p q) (C (C (N p) (K q (N q))) p))))