;;;; Propositional Calculus Tests ;;;; ;;;; File: propositional-calculus.in ;;;; Author: () ;;;; Version: 1 (load "propositional-calculus.lsp") ; Replace this line with your tests for EVALUATE. (wff? 'x) (wff? 't) (wff? ()) (wff? 5) (wff? '(not x)) (wff? '(not x y)) (wff? '(not 5)) (wff? '(not t)) (wff? '(and x)) (wff? '(and x y)) (wff? '(and x 5)) (wff? '(or x)) (wff? '(or x y)) (wff? '(or 5 y)) (wff? '(foo x)) (wff? '(foo x y)) (wff? '(and (not x) (or t (not y)))) (wff? '(and (not x) (or t (foo y)))) (wff? '(and (not x) (or (t y) (not y)))) (wff? '(and (not (not x)) (or (not y) f))) (wff? '(and (not (not x)) (not (not y) f))) (wff? '(and (not (and x)) (or (not y) f))) (assign '() '(and x (or y x))) (assign '((x b)) '(and x (or y x))) (assign '((x b) (y c)) '(and x (or y x))) (assign '((y c)) '(and x (or y x))) (assign '((x b)) '(not (and (or x y) (or y z)))) (assign '((x b) (y c)) '(not (and (or x y) (or y z)))) (assign '((z b) (y c)) '(not (and (or x y) (or y z)))) (assign '((r b) (s c)) '(not (and (or x y) (or y z)))) (one-variable 't) (one-variable 'x) (one-variable '(not x)) (one-variable '(and x (not y))) (one-variable '(and (or f (not y)) (not x))) (one-variable '(and (or f (not t)) (not x))) (one-variable '(and (or f (not t)) (not f))) ;; Two out of three are true or two out of three ;; are false. ;; (theorem?-1 '(or (and x y) (or (and y z) (or (and z x) (or (and (not x) (not y)) (or (and (not y) (not z)) (and (not z) (not x)))))))) ;; (implies (and p1 (and (implies p1 p2) ;; (implies p2 p3))) ;; p3)) ;; == (or (not (and p1 (and (or (not p1) p2) ;; (or (not p2) p3)))) ;; p3) ;; (theorem?-1 '(or (not (and p1 (and (or (not p1) p2) (or (not p2) p3)))) p3)) ;; (implies (and p1 (and (implies p1 p2) ;; (implies p3 p2))) ;; p3)) ;; == (or (not (and p1 (and (or (not p1) p2) ;; (or (not p3) p2)))) ;; p3) ;; (theorem?-1 '(or (not (and p1 (and (or (not p1) p2) (or (not p3) p2)))) p3)) ;; Pigeonhole Principle: If there are three pigeons and ;; two pigeon holes and every pigeon is in a hole, then ;; some hole has at least two pigeons. ;; ;; pij means pigeon i is in hole j. ;; ;; (implies (and (or p11 p12) ;; (and (or p21 p22) ;; (or p31 p32))) ;; (or (and p11 p21) ;; (or (and p21 p31) ;; (or (and p31 p11) ;; (or (and p12 p22) ;; (or (and p22 p32) ;; (and p32 p12))))))) ;; == ;; (or (not (and (or p11 p12) ;; (and (or p21 p22) ;; (or p31 p32)))) ;; (or (and p11 p21) ;; (or (and p21 p31) ;; (or (and p31 p11) ;; (or (and p12 p22) ;; (or (and p22 p32) ;; (and p32 p12))))))) ;; (theorem?-1 '(or (not (and (or p11 p12) (and (or p21 p22) (or p31 p32)))) (or (and p11 p21) (or (and p21 p31) (or (and p31 p11) (or (and p12 p22) (or (and p22 p32) (and p32 p12)))))))) (setf *trace* t) (dnf-distribute '(or (and x y) z)) (dnf-distribute '(or x (and y z))) (dnf-distribute '(and (or x y) z)) (dnf-distribute '(and x (or y z))) (dnf 'x) (dnf '(not x)) (dnf '(not (not x))) (dnf '(not (or x y))) (dnf '(not (and x y))) (dnf '(or (and x1 x2) (or (and y1 y2) (and z1 z2)))) (dnf '(and (or x1 x2) (and (or y1 y2) (or z1 z2)))) (setf *trace* nil) ;; Negation of: Two out of three are true or two out ;; of three are false. ;; (dnf '(not (or (and x y) (or (and y z) (or (and z x) (or (and (not x) (not y)) (or (and (not y) (not z)) (and (not z) (not x))))))))) ;; (not (implies (and p1 (and (implies p1 p2) ;; (implies p2 p3))) ;; p3)) ;; == (and p1 (and (or (not p1) p2) ;; (and (or (not p2) p3) ;; (not p3)))) ;; (dnf '(and p1 (and (or (not p1) p2) (and (or (not p2) p3) (not p3))))) ;; Pigeonhole Principle: If there are three pigeons and ;; two pigeon holes and every pigeon is in a hole, then ;; some hole has at least two pigeons. ;; ;; pij means pigeon i is in hole j. ;; ;; (implies (and (or p11 p12) ;; (and (or p21 p22) ;; (or p31 p32))) ;; (or (and p11 p21) ;; (or (and p21 p31) ;; (or (and p31 p11) ;; (or (and p12 p22) ;; (or (and p22 p32) ;; (and p32 p12))))))) ;; == ;; (or (not (and (or p11 p12) ;; (and (or p21 p22) ;; (or p31 p32)))) ;; (or (and p11 p21) ;; (or (and p21 p31) ;; (or (and p31 p11) ;; (or (and p12 p22) ;; (or (and p22 p32) ;; (and p32 p12))))))) ;; ;; Negate above before taking dnf. ;; (setf *print-level* 10) (dnf '(not (or (not (and (or p11 p12) (and (or p21 p22) (or p31 p32)))) (or (and p11 p21) (or (and p21 p31) (or (and p31 p11) (or (and p12 p22) (or (and p22 p32) (and p32 p12))))))))) (setf *print-level* 100) (literals 'x) (literals '(not x)) (literals '(and x (not y))) (literals '(or (not x) y)) (literals '(or x x)) (literals '(or (not x) (not x))) (literals '(or (and x (not z)) (and (not x) (not z)))) (negate 'x) (negate '(not x)) (unsatisfiable-dnf-clause 'x) (unsatisfiable-dnf-clause '(not x)) (unsatisfiable-dnf-clause '(and x (not x))) (unsatisfiable-dnf-clause '(and x (not y))) (unsatisfiable-dnf-clause '(and x x)) (unsatisfiable-dnf-clause '(and x (and y (and z (and (not x) w))))) (unsatisfiable-dnf-clause '(and x (and y (and z (and (not v) w))))) (unsatisfiable-dnf 'x) (unsatisfiable-dnf '(not x)) (unsatisfiable-dnf '(and x (not x))) (unsatisfiable-dnf '(or (and x (not y)) (and z w))) (unsatisfiable-dnf '(or (and x (not x)) (and z w))) (unsatisfiable-dnf '(or (and x (not y)) (and (not w) w))) (unsatisfiable-dnf '(or (and x (not y)) (and (not y) x))) (unsatisfiable-dnf '(or (and x (not x)) (and (not y) y))) ;; Two out of three are true or two out of three ;; are false. ;; (theorem?-2 '(or (and x y) (or (and y z) (or (and z x) (or (and (not x) (not y)) (or (and (not y) (not z)) (and (not z) (not x)))))))) ;; (implies (and p1 (and (implies p1 p2) ;; (implies p2 p3))) ;; p3) ;; == (or (not (and p1 (and (or (not p1) p2) ;; (or (not p2) p3)))) ;; p3) ;; (theorem?-2 '(or (not (and p1 (and (or (not p1) p2) (or (not p2) p3)))) p3)) ;; (implies (and p1 (and (implies p1 p2) ;; (implies p3 p2))) ;; p3)) ;; == (or (not (and p1 (and (or (not p1) p2) ;; (or (not p3) p2)))) ;; p3) ;; (theorem?-2 '(or (not (and p1 (and (or (not p1) p2) (or (not p3) p2)))) p3)) ;; Pigeonhole Principle: If there are three pigeons and ;; two pigeon holes and every pigeon is in a hole, then ;; some hole has at least two pigeons. ;; ;; pij means pigeon i is in hole j. ;; ;; (implies (and (or p11 p12) ;; (and (or p21 p22) ;; (or p31 p32))) ;; (or (and p11 p21) ;; (or (and p21 p31) ;; (or (and p31 p11) ;; (or (and p12 p22) ;; (or (and p22 p32) ;; (and p32 p12))))))) ;; == ;; (or (not (and (or p11 p12) ;; (and (or p21 p22) ;; (or p31 p32)))) ;; (or (and p11 p21) ;; (or (and p21 p31) ;; (or (and p31 p11) ;; (or (and p12 p22) ;; (or (and p22 p32) ;; (and p32 p12))))))) ;; (theorem?-2 '(or (not (and (or p11 p12) (and (or p21 p22) (or p31 p32)))) (or (and p11 p21) (or (and p21 p31) (or (and p31 p11) (or (and p12 p22) (or (and p22 p32) (and p32 p12))))))))