; By closer inspection of "prime tautologies" from my article
; `One hundred propositional tautologies (2)´, I noted that some of them are like
; (not (not (or true true)))
; It contains subformula (or true true), which is an instance of
; tautology
; (or true A).
; Hence, this formula doesn't say nothing new, but (not (not true)).
; and it should be removed from list of interesting tautologies.
; Generally, formula that has tautology as subformula (eccept
; trivial case - formula "true") is not interesting one. So, I
; decided to add one loop that will filter out such formulas from
; the list of 100 propositional tautologies, originally stored in
; prime-tautologies 1.
; The helper function, (lower-case-formula f) returns same formula as
; f, just with all upper-case symbols changed to lower case. I need
; it because lower case is used as constant in unify.
; Helper function
(set 'lower-case-formula
(lambda(f)
(cond ((list? f)(map lower-case-formula f))
((> (length (string f)) 1) f)
(true (sym (lower-case (string f)))))))
(set 'prime-tautologies1 (map lower-case-formula prime-tautologies1)) ; lower case - constants
(set 'prime-tautologies2 '())
(dolist(f1 prime-tautologies1)
(set 'found-instance nil)
(dolist(f2 prime-tautologies2 found-instance)
(dolist(f3 (branches f1) found-instance)
(unless(= f3 true) ; othervise every subformula true
; would be recognized as a special case.
(when (unify f3 f2)
(set 'found-instance true)
(println "formula " f1 ", subformula " f3 " is instance of " f2 ")" )))))
(unless found-instance
(push (upper-case-formula f1) prime-tautologies2 -1)))
(println "Filtered to " (length prime-tautologies2) ". prime tautologies2")
(map (lambda(x)(println $idx ". " x)) prime-tautologies2)
; Output:
; We started with 12971 formulas.
; Filtered to 2467 tautologies.
; Filtered to 350. prime tautologies1
;
; formula (not (not (or true true))), subformula (or true true) is instance of (or true A))
; formula (not (not (or true nil))), subformula (or true nil) is instance of (or true A))
; ...
; Filtered to 178. prime tautologies2
;
; 0. true
; 1. (not nil)
; 2. (not (not true))
; 3. (and true true)
; 4. (or true true)
; 5. (or true nil)
; 6. (or true A)
; 7. (or nil true)
; 8. (or A true)
; 9. (-> true true)
; 10. (-> nil true)
; 11. (-> nil nil)
; 12. (-> nil A)
; 13. (-> A true)
; 14. (-> A A)
; 15. (<-> true true)
; 16. (<-> nil nil)
; 17. (<-> A A)
; 18. (not (not (not nil)))
; 19. (not (and true nil))
; 20. (not (and nil true))
; 21. (not (and nil nil))
; 22. (not (and nil A))
; 23. (not (and A nil))
; 24. (not (or nil nil))
; 25. (not (-> true nil))
; 26. (not (<-> true nil))
; 27. (not (<-> nil true))
; 28. (and true (not nil))
; 29. (and (not nil) true)
; 30. (or nil (not nil))
; 31. (or A (not nil))
; 32. (or A (not A))
; 33. (or (not nil) nil)
; 34. (or (not nil) A)
; 35. (or (not A) A)
; 36. (-> true (not nil))
; 37. (-> A (not nil))
; 38. (-> (not true) nil)
; 39. (-> (not true) A)
; 40. (<-> true (not nil))
; 41. (<-> nil (not true))
; 42. (<-> (not true) nil)
; 43. (<-> (not nil) true)
; 44. (not (not (not (not true))))
; 45. (not (not (and true true)))
; 46. (not (and true (not true)))
; 47. (not (and A (not true)))
; 48. (not (and A (not A)))
; 49. (not (and (not true) true))
; 50. (not (and (not true) A))
; 51. (not (and (not A) A))
; 52. (not (or nil (not true)))
; 53. (not (or (not true) nil))
; 54. (not (-> true (not true)))
; 55. (not (-> (not nil) nil))
; 56. (not (<-> true (not true)))
; 57. (not (<-> nil (not nil)))
; 58. (not (<-> A (not A)))
; 59. (not (<-> (not true) true))
; 60. (not (<-> (not nil) nil))
; 61. (not (<-> (not A) A))
; 62. (and true (not (not true)))
; 63. (and true (and true true))
; 64. (and (not nil) (not nil))
; 65. (and (not (not true)) true)
; 66. (and (and true true) true)
; 67. (or nil (not (not true)))
; 68. (or nil (and true true))
; 69. (or A (not (not true)))
; 70. (or A (and true true))
; 71. (or A (-> A nil))
; 72. (or A (-> A B))
; 73. (or A (<-> nil A))
; 74. (or A (<-> A nil))
; 75. (or (not (not true)) nil)
; 76. (or (not (not true)) A)
; 77. (or (and true true) nil)
; 78. (or (and true true) A)
; 79. (or (-> A nil) A)
; 80. (or (-> A B) A)
; 81. (or (<-> nil A) A)
; 82. (or (<-> A nil) A)
; 83. (-> true (not (not true)))
; 84. (-> true (and true true))
; 85. (-> A (not (not true)))
; 86. (-> A (not (not A)))
; 87. (-> A (and true true))
; 88. (-> A (and true A))
; 89. (-> A (and A true))
; 90. (-> A (and A A))
; 91. (-> A (or nil A))
; 92. (-> A (or A nil))
; 93. (-> A (or A A))
; 94. (-> A (or A B))
; 95. (-> A (or B A))
; 96. (-> A (-> true A))
; 97. (-> A (-> B A))
; 98. (-> A (<-> true A))
; 99. (-> A (<-> A true))
; 100. (-> (not (not nil)) nil)
; 101. (-> (not (not nil)) A)
; 102. (-> (not (not A)) A)
; 103. (-> (and true nil) nil)
; 104. (-> (and true nil) A)
; 105. (-> (and true A) A)
; 106. (-> (and nil true) nil)
; 107. (-> (and nil true) A)
; 108. (-> (and nil nil) nil)
; 109. (-> (and nil nil) A)
; 110. (-> (and nil A) nil)
; 111. (-> (and nil A) A)
; 112. (-> (and nil A) B)
; 113. (-> (and A true) A)
; 114. (-> (and A nil) nil)
; 115. (-> (and A nil) A)
; 116. (-> (and A nil) B)
; 117. (-> (and A A) A)
; 118. (-> (and A B) A)
; 119. (-> (and A B) B)
; 120. (-> (or nil nil) nil)
; 121. (-> (or nil nil) A)
; 122. (-> (or nil A) A)
; 123. (-> (or A nil) A)
; 124. (-> (or A A) A)
; 125. (-> (-> true nil) nil)
; 126. (-> (-> true nil) A)
; 127. (-> (-> true A) A)
; 128. (-> (<-> true nil) nil)
; 129. (-> (<-> true nil) A)
; 130. (-> (<-> true A) A)
; 131. (-> (<-> nil true) nil)
; 132. (-> (<-> nil true) A)
; 133. (-> (<-> A true) A)
; 134. (<-> true (not (not true)))
; 135. (<-> true (and true true))
; 136. (<-> nil (not (not nil)))
; 137. (<-> nil (and true nil))
; 138. (<-> nil (and nil true))
; 139. (<-> nil (and nil nil))
; 140. (<-> nil (and nil A))
; 141. (<-> nil (and A nil))
; 142. (<-> nil (or nil nil))
; 143. (<-> nil (-> true nil))
; 144. (<-> nil (<-> true nil))
; 145. (<-> nil (<-> nil true))
; 146. (<-> A (not (not A)))
; 147. (<-> A (and true A))
; 148. (<-> A (and A true))
; 149. (<-> A (and A A))
; 150. (<-> A (or nil A))
; 151. (<-> A (or A nil))
; 152. (<-> A (or A A))
; 153. (<-> A (-> true A))
; 154. (<-> A (<-> true A))
; 155. (<-> A (<-> A true))
; 156. (<-> (not (not true)) true)
; 157. (<-> (not (not nil)) nil)
; 158. (<-> (not (not A)) A)
; 159. (<-> (and true true) true)
; 160. (<-> (and true nil) nil)
; 161. (<-> (and true A) A)
; 162. (<-> (and nil true) nil)
; 163. (<-> (and nil nil) nil)
; 164. (<-> (and nil A) nil)
; 165. (<-> (and A true) A)
; 166. (<-> (and A nil) nil)
; 167. (<-> (and A A) A)
; 168. (<-> (or nil nil) nil)
; 169. (<-> (or nil A) A)
; 170. (<-> (or A nil) A)
; 171. (<-> (or A A) A)
; 172. (<-> (-> true nil) nil)
; 173. (<-> (-> true A) A)
; 174. (<-> (<-> true nil) nil)
; 175. (<-> (<-> true A) A)
; 176. (<-> (<-> nil true) nil)
; 177. (<-> (<-> A true) A)
;
---
No comments:
Post a Comment