; I write program that derives one hundred propositional tautologies. ; Then I identify one which is not interesting, and try to improve ; program so next time it derives one hundred of more interesting ; propositional tautologies. We'll see where is this going. ; ; ; Preparing part: (load "http://www.instprog.com/Instprog.default-library.lsp") (set '*list (lambda(l1 l2) (let ((result '())) (dolist(i l1) (dolist(j l2) (push (list i j) result -1))) result))) (set 'appendall (lambda(a b) (apply append (map a b)))) (set 'all-pf (lambda(len leafs unary binary) (if (= len 1) leafs (append (appendall (lambda(connective) (map (lambda(x)(list connective x)) (all-pf (- len 1) leafs unary binary))) unary) (if (> len 2) (appendall (lambda(connective) (appendall (lambda(r) (map (lambda(x)(cons connective x)) (*list (all-pf r leafs unary binary) (all-pf (- len 1 r) leafs unary binary)))) (sequence 1 (- len 2)))) binary) '()))))) (set 'element find) (set 'size-pf (lambda(f) (if (list? f) (apply + (map size-pf f)) 1))) ; For the first time, I has the right on a wild guess. So, I'll ; of the length 3 and 4, using true, nil and variables a b c d e, ; and classical connectives and filter tautologies. (---) (set 'tautologies (filter tautology? (append (all-pf 3 '(true nil a b c d e) '(not) '(and or -> <->)) (all-pf 4 '(true nil a b c d e) '(not) '(and or -> <->))))) (map (lambda(x)(println (+ $idx 1) ". " x)) tautologies) ;=============================================================== ; ; RESULTS: 1. (not (not true)) 2. (and true true) 3. (or true true) 4. (or true nil) 5. (or true a) 6. (or true b) 7. (or true c) 8. (or true d) 9. (or true e) 10. (or nil true) 11. (or a true) 12. (or b true) 13. (or c true) 14. (or d true) 15. (or e true) 16. (-> true true) 17. (-> nil true) 18. (-> nil nil) 19. (-> nil a) 20. (-> nil b) 21. (-> nil c) 22. (-> nil d) 23. (-> nil e) 24. (-> a true) 25. (-> a a) 26. (-> b true) 27. (-> b b) 28. (-> c true) 29. (-> c c) 30. (-> d true) 31. (-> d d) 32. (-> e true) 33. (-> e e) 34. (<-> true true) 35. (<-> nil nil) 36. (<-> a a) 37. (<-> b b) 38. (<-> c c) 39. (<-> d d) 40. (<-> e e) 41. (not (not (not nil))) 42. (not (and true nil)) 43. (not (and nil true)) 44. (not (and nil nil)) 45. (not (and nil a)) 46. (not (and nil b)) 47. (not (and nil c)) 48. (not (and nil d)) 49. (not (and nil e)) 50. (not (and a nil)) 51. (not (and b nil)) 52. (not (and c nil)) 53. (not (and d nil)) 54. (not (and e nil)) 55. (not (or nil nil)) 56. (not (-> true nil)) 57. (not (<-> true nil)) 58. (not (<-> nil true)) 59. (and true (not nil)) 60. (and (not nil) true) 61. (or true (not true)) 62. (or true (not nil)) 63. (or true (not a)) 64. (or true (not b)) 65. (or true (not c)) 66. (or true (not d)) 67. (or true (not e)) 68. (or nil (not nil)) 69. (or a (not nil)) 70. (or a (not a)) 71. (or b (not nil)) 72. (or b (not b)) 73. (or c (not nil)) 74. (or c (not c)) 75. (or d (not nil)) 76. (or d (not d)) 77. (or e (not nil)) 78. (or e (not e)) 79. (or (not true) true) 80. (or (not nil) true) 81. (or (not nil) nil) 82. (or (not nil) a) 83. (or (not nil) b) 84. (or (not nil) c) 85. (or (not nil) d) 86. (or (not nil) e) 87. (or (not a) true) 88. (or (not a) a) 89. (or (not b) true) 90. (or (not b) b) 91. (or (not c) true) 92. (or (not c) c) 93. (or (not d) true) 94. (or (not d) d) 95. (or (not e) true) 96. (or (not e) e) 97. (-> true (not nil)) 98. (-> nil (not true)) 99. (-> nil (not nil)) 100. (-> nil (not a)) 101. (-> nil (not b)) 102. (-> nil (not c)) 103. (-> nil (not d)) 104. (-> nil (not e)) 105. (-> a (not nil)) 106. (-> b (not nil)) 107. (-> c (not nil)) 108. (-> d (not nil)) 109. (-> e (not nil)) 110. (-> (not true) true) 111. (-> (not true) nil) 112. (-> (not true) a) 113. (-> (not true) b) 114. (-> (not true) c) 115. (-> (not true) d) 116. (-> (not true) e) 117. (-> (not nil) true) 118. (-> (not a) true) 119. (-> (not b) true) 120. (-> (not c) true) 121. (-> (not d) true) 122. (-> (not e) true) 123. (<-> true (not nil)) 124. (<-> nil (not true)) 125. (<-> (not true) nil) 126. (<-> (not nil) true) Even for this, very first attempt, some interesting formulas are derived. For example, 5. (or true a) 11. (or a true) 19. (-> nil a) lie implies anything 24. (-> a true) anything implies truth 25. (-> a a) reflexivity of implication 36. (<-> a a) reflexivity of equivalence 45. (not (and nil a)) 50. (not (and a nil)) 70. (or a (not a)) (not a) is right inverse of a 88. (or (not a) a) (not a) is left inverse of a So, 10 interesting out of 126 tautologies. Not that bad. The first tautology that is not interesting is 6. (or true b), because difference in the name of the variable appears not to be significant enough. Next thing to do is to filter tautologies and keep only those that cannot be obtained from other tautologies by simple rename of the variables. |
I wonder if it's time for you to split up the 3000 line library into more than one file... ? I wanted to use debug-wrap, but kept on getting pages of tautologies.. :) And I couldn't work out how to suppress the printing...
ReplyDeletecormullion
Cormullion,
ReplyDeletemaybe you're right but I prolong it, because my experience in the past was that it will only become more complicated if I'd have to take care about order of the load. Anycase, it appears to work for me (although version on the net lags behind things described on the blog).
(load "http://www.instprog.com/Instprog.default-library.lsp")
(debug-wrap fibo)
(fibo 4)
(set 'print.supressed true)
(print "supressed" " is " " it")
(set 'print.supressed false)
(print "isnt supressed" " this " " is")
(exit)
Note that print is now macro, hence it wouldn't work with (args) or $idx any more after my library is loaded.
If you find some relatively simple code where it doesn't work, please, post it to me.
Thank you for opinion.