One Hundred Propositional Tautologies (2)

;
; In previous, the first post of this serial, I simply defined few hundreds
; tautologies and checked whether they are tautologies. However,
; it was obvious that there are many of duplicates that differed
; only in using different variables. This time, we'll try to filter
; these tautologies, so these duplicated are rejected. First, we'll
; define the base of the formulas and tautologies.
;

(load "C:\\Newlisp\\Instprog.default-library.lsp")    

(set 'formulas (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 -> <->))
                                 
                       (all-pf 5 '(true nil a b c d e)
                                 '(not)
                                 '(and or -> <->))))
                                 
(println "We started with " (length formulas) ". formulas.")                                                     

(set 'tautologies (filter tautology? formulas))

(println "Filtered to " (length tautologies) ". tautologies.")
                                                       
; I'll define the notion of the "prime tautology", in analogy to
; the prime numbers. Let us assume that tautologies are ordered
; in the list t1, t2, t3, ....

; the prime tautology is tautology that is not *an instance* of
; some other tautology that occured on the earlier place in the
; list.
;
; What does it mean that tautology (or more generally, the formula)
; f2 is "an instance" of other formula f1? Intuitively, that means
; that f2 is the special case of the more general formula f1. Just
; like in natural language, "London cathedral" is a special case of
; "Christian church."
;
; For example, (and (or x y) (not z)) is an instance of (and a b), because
; the substitution of a with (or x y), and b with (not z) will result in
; (and (or x y) z). Similarly, (or (and x y) (not z)) is not an instance
; of (and a b), because no substitution can transform that top level
; "and" into top-level "or."
;
; How can we check whether tautology t1 is instance of the tautology t2?
; First, because of technical reasons we should ensure that variables used
; in t1 are different than variables used in t2. Humans can understand
; that formula (or (not x) (not y)) is a special case of (or x y),
; because he'll understand that x and y are used in two different
; contexts, but with computers, this only complicates the issue.
;
; Because of that, we'll first change the form (or x y) into (or X Y),
; ie., we'll replace lowercase variables with uppercase.

(set 'upper-case-formula
     (lambda(f)
       (cond ((list? f)(map upper-case-formula f))
             ((> (length (string f)) 1) f)  
             (true (sym (upper-case (string f)))))))
             
; Now, we'll filter tautologies; we'll define another list, prime-tautologies,
; initially empty. Then, we'll take tautologies from the list, and
; check, one by one, whether these are instances of some of the
; formulas from prime-tautologies. If it is not, they will be
; added to prime tautologies.
;

; But, how can we check whether formula f is an instance of some
; other formula g? It would be the most complicated part. Fortunately,
; Newlisp has more general functions - unify. Unify doesn't test
; whether there is a substition s, such that f=s(g), but whether
; there is "unification" u, such that u(f)=u(g). During such test,
; unify will consider *only* symbols starting with upper case as variables.

(println (unify '(or (not x) (not y)) '(or X Y)))  ; ((X (not x)) (Y (not y)))
(println (unify '(or (not x) (not y)) '(and X Y))) ; nil

(set 'prime-tautologies '())
(dolist(f1 tautologies)
   (set 'composite nil)
   (dolist(f2 prime-tautologies composite)
      (if (unify f1 f2)
          (set 'composite true)))
   (when (not composite)
         (push (upper-case-formula f1) prime-tautologies -1)))

(println "Filtered to " (length tautologies) ". prime tautologies")

(map (lambda(x)(print $idx ". " x)) prime-tautologies)
(exit)

; RESULTS
;
; Now, this is pure beauty. All important formulas, if short enough
; are here. Among others, controversial (-> A (not (not A))) and 
; (-> (not (not A)) A). I cannot, however, decide whether formulas 
; containing only constants are interesting. Clearly, (not (not true)) 
; is interesting formula, but what with others? (not (not (not nil))) 
; looks as less interesting, but why? 

We started with 12957. formulas.
Filtered to 2465. tautologies.
Filtered to 348. prime tautologies
0. (not (not true))
1. (and true true)
2. (or true true)
3. (or true nil)
4. (or true A)
5. (or nil true)
6. (or A true)
7. (-> true true)
8. (-> nil true)
9. (-> nil nil)
10. (-> nil A)
11. (-> A true)
12. (-> A A)
13. (<-> true true)
14. (<-> nil nil)
15. (<-> A A)
16. (not (not (not nil)))
17. (not (and true nil))
18. (not (and nil true))
19. (not (and nil nil))
20. (not (and nil A))
21. (not (and A nil))
22. (not (or nil nil))
23. (not (-> true nil))
24. (not (<-> true nil))
25. (not (<-> nil true))
26. (and true (not nil))
27. (and (not nil) true)
28. (or nil (not nil))
29. (or A (not nil))
30. (or A (not A))
31. (or (not nil) nil)
32. (or (not nil) A)
33. (or (not A) A)
34. (-> true (not nil))
35. (-> A (not nil))
36. (-> (not true) nil)
37. (-> (not true) A)
38. (<-> true (not nil))
39. (<-> nil (not true))
40. (<-> (not true) nil)
41. (<-> (not nil) true)
42. (not (not (not (not true))))
43. (not (not (and true true)))
44. (not (not (or true true)))
45. (not (not (or true nil)))
46. (not (not (or true A)))
47. (not (not (or nil true)))
48. (not (not (or A true)))
49. (not (not (-> true true)))
50. (not (not (-> nil true)))
51. (not (not (-> nil nil)))
52. (not (not (-> nil A)))
53. (not (not (-> A true)))
54. (not (not (-> A A)))
55. (not (not (<-> true true)))
56. (not (not (<-> nil nil)))
57. (not (not (<-> A A)))
58. (not (and true (not true)))
59. (not (and A (not true)))
60. (not (and A (not A)))
61. (not (and (not true) true))
62. (not (and (not true) A))
63. (not (and (not A) A))
64. (not (or nil (not true)))
65. (not (or (not true) nil))
66. (not (-> true (not true)))
67. (not (-> (not nil) nil))
68. (not (<-> true (not true)))
69. (not (<-> nil (not nil)))
70. (not (<-> A (not A)))
71. (not (<-> (not true) true))
72. (not (<-> (not nil) nil))
73. (not (<-> (not A) A))
74. (and true (not (not true)))
75. (and true (and true true))
76. (and true (or true true))
77. (and true (or true nil))
78. (and true (or true A))
79. (and true (or nil true))
80. (and true (or A true))
81. (and true (-> true true))
82. (and true (-> nil true))
83. (and true (-> nil nil))
84. (and true (-> nil A))
85. (and true (-> A true))
86. (and true (-> A A))
87. (and true (<-> true true))
88. (and true (<-> nil nil))
89. (and true (<-> A A))
90. (and (not nil) (not nil))
91. (and (not (not true)) true)
92. (and (and true true) true)
93. (and (or true true) true)
94. (and (or true nil) true)
95. (and (or true A) true)
96. (and (or nil true) true)
97. (and (or A true) true)
98. (and (-> true true) true)
99. (and (-> nil true) true)
100. (and (-> nil nil) true)
101. (and (-> nil A) true)
102. (and (-> A true) true)
103. (and (-> A A) true)
104. (and (<-> true true) true)
105. (and (<-> nil nil) true)
106. (and (<-> A A) true)
107. (or nil (not (not true)))
108. (or nil (and true true))
109. (or nil (or true true))
110. (or nil (or true nil))
111. (or nil (or true A))
112. (or nil (or nil true))
113. (or nil (or A true))
114. (or nil (-> true true))
115. (or nil (-> nil true))
116. (or nil (-> nil nil))
117. (or nil (-> nil A))
118. (or nil (-> A true))
119. (or nil (-> A A))
120. (or nil (<-> true true))
121. (or nil (<-> nil nil))
122. (or nil (<-> A A))
123. (or A (not (not true)))
124. (or A (and true true))
125. (or A (or true true))
126. (or A (or true nil))
127. (or A (or true A))
128. (or A (or true B))
129. (or A (or nil true))
130. (or A (or A true))
131. (or A (or B true))
132. (or A (-> true true))
133. (or A (-> nil true))
134. (or A (-> nil nil))
135. (or A (-> nil A))
136. (or A (-> nil B))
137. (or A (-> A true))
138. (or A (-> A nil))
139. (or A (-> A A))
140. (or A (-> A B))
141. (or A (-> B true))
142. (or A (-> B B))
143. (or A (<-> true true))
144. (or A (<-> nil nil))
145. (or A (<-> nil A))
146. (or A (<-> A nil))
147. (or A (<-> A A))
148. (or A (<-> B B))
149. (or (not (not true)) nil)
150. (or (not (not true)) A)
151. (or (and true true) nil)
152. (or (and true true) A)
153. (or (or true true) nil)
154. (or (or true true) A)
155. (or (or true nil) nil)
156. (or (or true nil) A)
157. (or (or true A) nil)
158. (or (or true A) A)
159. (or (or true A) B)
160. (or (or nil true) nil)
161. (or (or nil true) A)
162. (or (or A true) nil)
163. (or (or A true) A)
164. (or (or A true) B)
165. (or (-> true true) nil)
166. (or (-> true true) A)
167. (or (-> nil true) nil)
168. (or (-> nil true) A)
169. (or (-> nil nil) nil)
170. (or (-> nil nil) A)
171. (or (-> nil A) nil)
172. (or (-> nil A) A)
173. (or (-> nil A) B)
174. (or (-> A true) nil)
175. (or (-> A true) A)
176. (or (-> A true) B)
177. (or (-> A nil) A)
178. (or (-> A A) nil)
179. (or (-> A A) A)
180. (or (-> A A) B)
181. (or (-> A B) A)
182. (or (<-> true true) nil)
183. (or (<-> true true) A)
184. (or (<-> nil nil) nil)
185. (or (<-> nil nil) A)
186. (or (<-> nil A) A)
187. (or (<-> A nil) A)
188. (or (<-> A A) nil)
189. (or (<-> A A) A)
190. (or (<-> A A) B)
191. (-> true (not (not true)))
192. (-> true (and true true))
193. (-> true (or true true))
194. (-> true (or true nil))
195. (-> true (or true A))
196. (-> true (or nil true))
197. (-> true (or A true))
198. (-> true (-> true true))
199. (-> true (-> nil true))
200. (-> true (-> nil nil))
201. (-> true (-> nil A))
202. (-> true (-> A true))
203. (-> true (-> A A))
204. (-> true (<-> true true))
205. (-> true (<-> nil nil))
206. (-> true (<-> A A))
207. (-> A (not (not true)))
208. (-> A (not (not A)))
209. (-> A (and true true))
210. (-> A (and true A))
211. (-> A (and A true))
212. (-> A (and A A))
213. (-> A (or true true))
214. (-> A (or true nil))
215. (-> A (or true A))
216. (-> A (or true B))
217. (-> A (or nil true))
218. (-> A (or nil A))
219. (-> A (or A true))
220. (-> A (or A nil))
221. (-> A (or A A))
222. (-> A (or A B))
223. (-> A (or B true))
224. (-> A (or B A))
225. (-> A (-> true true))
226. (-> A (-> true A))
227. (-> A (-> nil true))
228. (-> A (-> nil nil))
229. (-> A (-> nil A))
230. (-> A (-> nil B))
231. (-> A (-> A true))
232. (-> A (-> A A))
233. (-> A (-> B true))
234. (-> A (-> B A))
235. (-> A (-> B B))
236. (-> A (<-> true true))
237. (-> A (<-> true A))
238. (-> A (<-> nil nil))
239. (-> A (<-> A true))
240. (-> A (<-> A A))
241. (-> A (<-> B B))
242. (-> (not (not nil)) nil)
243. (-> (not (not nil)) A)
244. (-> (not (not A)) A)
245. (-> (and true nil) nil)
246. (-> (and true nil) A)
247. (-> (and true A) A)
248. (-> (and nil true) nil)
249. (-> (and nil true) A)
250. (-> (and nil nil) nil)
251. (-> (and nil nil) A)
252. (-> (and nil A) nil)
253. (-> (and nil A) A)
254. (-> (and nil A) B)
255. (-> (and A true) A)
256. (-> (and A nil) nil)
257. (-> (and A nil) A)
258. (-> (and A nil) B)
259. (-> (and A A) A)
260. (-> (and A B) A)
261. (-> (and A B) B)
262. (-> (or nil nil) nil)
263. (-> (or nil nil) A)
264. (-> (or nil A) A)
265. (-> (or A nil) A)
266. (-> (or A A) A)
267. (-> (-> true nil) nil)
268. (-> (-> true nil) A)
269. (-> (-> true A) A)
270. (-> (<-> true nil) nil)
271. (-> (<-> true nil) A)
272. (-> (<-> true A) A)
273. (-> (<-> nil true) nil)
274. (-> (<-> nil true) A)
275. (-> (<-> A true) A)
276. (<-> true (not (not true)))
277. (<-> true (and true true))
278. (<-> true (or true true))
279. (<-> true (or true nil))
280. (<-> true (or true A))
281. (<-> true (or nil true))
282. (<-> true (or A true))
283. (<-> true (-> true true))
284. (<-> true (-> nil true))
285. (<-> true (-> nil nil))
286. (<-> true (-> nil A))
287. (<-> true (-> A true))
288. (<-> true (-> A A))
289. (<-> true (<-> true true))
290. (<-> true (<-> nil nil))
291. (<-> true (<-> A A))
292. (<-> nil (not (not nil)))
293. (<-> nil (and true nil))
294. (<-> nil (and nil true))
295. (<-> nil (and nil nil))
296. (<-> nil (and nil A))
297. (<-> nil (and A nil))
298. (<-> nil (or nil nil))
299. (<-> nil (-> true nil))
300. (<-> nil (<-> true nil))
301. (<-> nil (<-> nil true))
302. (<-> A (not (not A)))
303. (<-> A (and true A))
304. (<-> A (and A true))
305. (<-> A (and A A))
306. (<-> A (or nil A))
307. (<-> A (or A nil))
308. (<-> A (or A A))
309. (<-> A (-> true A))
310. (<-> A (<-> true A))
311. (<-> A (<-> A true))
312. (<-> (not (not true)) true)
313. (<-> (not (not nil)) nil)
314. (<-> (not (not A)) A)
315. (<-> (and true true) true)
316. (<-> (and true nil) nil)
317. (<-> (and true A) A)
318. (<-> (and nil true) nil)
319. (<-> (and nil nil) nil)
320. (<-> (and nil A) nil)
321. (<-> (and A true) A)
322. (<-> (and A nil) nil)
323. (<-> (and A A) A)
324. (<-> (or true true) true)
325. (<-> (or true nil) true)
326. (<-> (or true A) true)
327. (<-> (or nil true) true)
328. (<-> (or nil nil) nil)
329. (<-> (or nil A) A)
330. (<-> (or A true) true)
331. (<-> (or A nil) A)
332. (<-> (or A A) A)
333. (<-> (-> true true) true)
334. (<-> (-> true nil) nil)
335. (<-> (-> true A) A)
336. (<-> (-> nil true) true)
337. (<-> (-> nil nil) true)
338. (<-> (-> nil A) true)
339. (<-> (-> A true) true)
340. (<-> (-> A A) true)
341. (<-> (<-> true true) true)
342. (<-> (<-> true nil) nil)
343. (<-> (<-> true A) A)
344. (<-> (<-> nil true) nil)
345. (<-> (<-> nil nil) true)
346. (<-> (<-> A true) A)
347. (<-> (<-> A A) true)
 

---