Kazimir Majorinc's Programming Notes.

Relatively Short Propositional Formulas and Symbols Instead of Pointers and Tables.

; Boolean functions are functions from set {0, 1} to set {0, 1}.
; Our well known logical connectives and, or and not are such
; Boolean functions. In usual mathematical notation, it would be
; written:
;
;         or(0,0)=0; or(0,1)=1; or(1,0)=1; or(1,1)=1.
;
; Frequently, Booleans functions are defined in the form of the
; "truth-table".
;
;                   a b (or a b)
;                  ---------------
;                   0 0    0
;                   0 1    1
;                   1 0    1
;                   1 1    1
;
; Boolean function is determined by third column, in this case,
; 0111. For each Boolean function, there are many possible formulas
; that define the function. In our example (or a b), but also
; (not (and a b)), (and (not a) (not b)), (-> (not a) b), and
; many others. Boolean functions and propositional formulas are very
; important, because computers are machines that calculate boolean
; functions, using physical realization of proposition formulas.
;
; The following program analyzes given list of all propositional
; formulas, and search for minimal between equivalent formulas.
;
; For all formulas f in list (f0 f1 ... fn),
;
;   (i) Boolean function B defined with f is found
;   (ii) it is tested whether f is a first formula that defines B,
;        or it is shorter than other formulas defining B.
;
; The program builds data structure, defining and using symbols.
; For example, if list ((or a b) (not (and a b)) (-> (not a) b)) is
; given, the program would first found that (or a b) defines Boolean
; function given with column 0111 in truth table. Then it would define
; two symbols and values:
;
;     [Boolean-function.0111] => ((or a b))
;     [propositional-formulas.(or a b)] => [Boolean-function.0111]
;
; After that, (not (and a b)) is found to define same Boolean function,
; but it is longer than (or a b), so nothing changes. If some shorter
; formula defining same Boolean function is found, then
; value [Boolean-function.0111] would be redefined.
;
; In this program, symbols are used instead of hash tables, in some
; other languages, where syntax would be something like
; Boolean-function[0111] instead. One might be surprised with such
; use of the symbols, and think it is abuse of the symbols. But,
; I think it is actually apropriate use, because, in general case,
; there is no reasons for distinction between hash table name,
; and key.
;
; In following program, such procedure is applied on all formulas
; with seven or less "nodes", and finally, all defined Boolean
; functions, and shortest formulas defining these Boolean functions
; are printed.

(set '[println.supressed] true '[print.supressed] true)
(load "http://www.instprog.com/Instprog.default-library.lsp")
(set '[println.supressed] nil '[print.supressed] nil)

(set 'PF (apply append (map (lambda(x)(all-pf x '(true nil A B C)
                                                '(not)
                                                '(and or -> <->)))
                            (sequence 1 7))))

(box-standard "Generated " (length PF) " formulas.")

(set 'truth-column
     (lambda(f)(let ((result '()))
                    (letex((L (propositional-variables f)))
                          (dolist-multi(L '(nil true))
                             (push (eval f) result -1))
                    result))))

(set 'truth-column01
     (lambda(f)(apply string (map (lambda(x)(if x "1" "0"))
                                  (truth-column f)))))

(set 'symexpr (lambda()
                 (let ((result "["))
                      (dolist(i (args))
                        (set 'result (append result (string i) ".")))
                      (setf (last result) "]")
                      (sym result))))

(dolist(formula PF)
  (dolist(subformula (branches formula)) ; for formulas, branches are subformulas

    (set 'canonized-subformula (canon subformula)) ; canon: variables occur in alphabetical order

    (set 'canonized-subformula-symbol
         (symexpr "propositional-formula" canonized-subformula))

    (if (= (eval canonized-subformula-symbol) nil)

        ; new canonized subformula

       (begin (set 'Boolean-function-symbol
                   (symexpr "Boolean-function" (truth-column01 canonized-subformula)))

              (set canonized-subformula-symbol Boolean-function-symbol)

              (if (= (eval Boolean-function-symbol) nil)

                  ; new category

                  (set Boolean-function-symbol (list canonized-subformula))

                  ; old category

                  (if (< (size canonized-subformula)   ;new formula is leader of subcategory
                         (size (first (eval Boolean-function-symbol))))

                       ; canonized subformula is the best represent of category

                       (set Boolean-function-symbol (list canonized-subformula))

                       ; canonized subformula isn't the best represent of category

                       "do nothing")))

          ;old canonized subformula

          "do nothing")))

(set 'counter 1)
(dolist(formula PF)
  (when (= formula (canon formula))
     (set 'propositional-formula-symbol (symexpr "propositional-formula" formula))
     (set 'Boolean-function-symbol (symexpr "Boolean-function" (truth-column01 formula)))
     (when (= formula (first (eval Boolean-function-symbol)))
           (println counter ". " formula ", " Boolean-function-symbol)
           (inc counter))))
(exit)

                      +------------------+
                      | Generated 287535 |
                      |    formulas.     |
                      +------------------+

1. true, [Boolean-function.1]
2. nil, [Boolean-function.0]
3. A, [Boolean-function.01]
4. (not A), [Boolean-function.10]
5. (and nil A), [Boolean-function.00]
6. (and A B), [Boolean-function.0001]
7. (or true A), [Boolean-function.11]
8. (or A B), [Boolean-function.0111]
9. (-> A B), [Boolean-function.1101]
10. (<-> A B), [Boolean-function.1001]
11. (not (and A B)), [Boolean-function.1110]
12. (not (or A B)), [Boolean-function.1000]
13. (not (-> A B)), [Boolean-function.0010]
14. (not (<-> A B)), [Boolean-function.0110]
15. (and (not A) B), [Boolean-function.0100]
16. (or A (not B)), [Boolean-function.1011]
17. (and nil (and A B)), [Boolean-function.0000]
18. (and A (and B C)), [Boolean-function.00000001]
19. (and A (or true B)), [Boolean-function.0011]
20. (and A (or B C)), [Boolean-function.00000111]
21. (and A (-> B C)), [Boolean-function.00001101]
22. (and A (<-> B C)), [Boolean-function.00001001]
23. (and (or true A) B), [Boolean-function.0101]
24. (and (or A B) C), [Boolean-function.00010101]
25. (and (-> A B) C), [Boolean-function.01010001]
26. (and (<-> A B) C), [Boolean-function.01000001]
27. (or true (and A B)), [Boolean-function.1111]
28. (or A (and B C)), [Boolean-function.00011111]
29. (or A (or B C)), [Boolean-function.01111111]
30. (or A (-> B C)), [Boolean-function.11011111]
31. (or A (<-> B C)), [Boolean-function.10011111]
32. (or (and A B) C), [Boolean-function.01010111]
33. (or (-> A B) C), [Boolean-function.11110111]
34. (or (<-> A B) C), [Boolean-function.11010111]
35. (-> A (and nil B)), [Boolean-function.1100]
36. (-> A (and B C)), [Boolean-function.11110001]
37. (-> A (-> B C)), [Boolean-function.11111101]
38. (-> A (<-> B C)), [Boolean-function.11111001]
39. (-> (or A B) C), [Boolean-function.11010101]
40. (-> (-> A B) C), [Boolean-function.01011101]
41. (-> (<-> A B) C), [Boolean-function.01111101]
42. (<-> A (and B C)), [Boolean-function.11100001]
43. (<-> A (or B C)), [Boolean-function.10000111]
44. (<-> A (-> B C)), [Boolean-function.00101101]
45. (<-> A (<-> B C)), [Boolean-function.01101001]
46. (<-> (and nil A) B), [Boolean-function.1010]
47. (<-> (and A B) C), [Boolean-function.10101001]
48. (<-> (or A B) C), [Boolean-function.10010101]
49. (<-> (-> A B) C), [Boolean-function.01011001]
50. (not (and A (and B C))), [Boolean-function.11111110]
51. (not (and A (or B C))), [Boolean-function.11111000]
52. (not (and A (-> B C))), [Boolean-function.11110010]
53. (not (and A (<-> B C))), [Boolean-function.11110110]
54. (not (and (or A B) C)), [Boolean-function.11101010]
55. (not (and (-> A B) C)), [Boolean-function.10101110]
56. (not (and (<-> A B) C)), [Boolean-function.10111110]
57. (not (or A (and B C))), [Boolean-function.11100000]
58. (not (or A (or B C))), [Boolean-function.10000000]
59. (not (or A (-> B C))), [Boolean-function.00100000]
60. (not (or A (<-> B C))), [Boolean-function.01100000]
61. (not (or (and A B) C)), [Boolean-function.10101000]
62. (not (or (-> A B) C)), [Boolean-function.00001000]
63. (not (or (<-> A B) C)), [Boolean-function.00101000]
64. (not (-> A (and B C))), [Boolean-function.00001110]
65. (not (-> A (-> B C))), [Boolean-function.00000010]
66. (not (-> A (<-> B C))), [Boolean-function.00000110]
67. (not (-> (or A B) C)), [Boolean-function.00101010]
68. (not (-> (-> A B) C)), [Boolean-function.10100010]
69. (not (-> (<-> A B) C)), [Boolean-function.10000010]
70. (not (<-> A (and B C))), [Boolean-function.00011110]
71. (not (<-> A (or B C))), [Boolean-function.01111000]
72. (not (<-> A (-> B C))), [Boolean-function.11010010]
73. (not (<-> A (<-> B C))), [Boolean-function.10010110]
74. (not (<-> (and A B) C)), [Boolean-function.01010110]
75. (not (<-> (or A B) C)), [Boolean-function.01101010]
76. (not (<-> (-> A B) C)), [Boolean-function.10100110]
77. (and A (and (not B) C)), [Boolean-function.00000100]
78. (and A (or B (not C))), [Boolean-function.00001011]
79. (and (not A) (and B C)), [Boolean-function.00010000]
80. (and (not A) (or B C)), [Boolean-function.01110000]
81. (and (not A) (-> B C)), [Boolean-function.11010000]
82. (and (not A) (<-> B C)), [Boolean-function.10010000]
83. (and (not (and A B)) C), [Boolean-function.01010100]
84. (and (not (or A B)) C), [Boolean-function.01000000]
85. (and (not (<-> A B)) C), [Boolean-function.00010100]
86. (and (or A (not B)) C), [Boolean-function.01000101]
87. (or A (not (and B C))), [Boolean-function.11101111]
88. (or A (not (or B C))), [Boolean-function.10001111]
89. (or A (not (-> B C))), [Boolean-function.00101111]
90. (or A (not (<-> B C))), [Boolean-function.01101111]
91. (or A (and (not B) C)), [Boolean-function.01001111]
92. (or A (or B (not C))), [Boolean-function.10111111]
93. (or (and A B) (not C)), [Boolean-function.10101011]
94. (or (-> A B) (not C)), [Boolean-function.11111011]
95. (or (<-> A B) (not C)), [Boolean-function.11101011]
96. (or (and (not A) B) C), [Boolean-function.01110101]
97. (-> A (and (not B) C)), [Boolean-function.11110100]
98. (<-> A (and (not B) C)), [Boolean-function.10110100]
99. (<-> A (or B (not C))), [Boolean-function.01001011]
100. (<-> (and (not A) B) C), [Boolean-function.10011010]
101. (<-> (or A (not B)) C), [Boolean-function.01100101]
102. (not (and (or A (not B)) C)), [Boolean-function.10111010]
103. (not (or A (and (not B) C))), [Boolean-function.10110000]
104. (not (or (and (not A) B) C)), [Boolean-function.10001010]
105. (and nil (and A (and B C))), [Boolean-function.00000000]
106. (and A (and B (or true C))), [Boolean-function.00000011]
107. (and A (and (or true B) C)), [Boolean-function.00000101]
108. (and A (or true (and B C))), [Boolean-function.00001111]
109. (and A (-> B (and nil C))), [Boolean-function.00001100]
110. (and A (<-> (and nil B) C)), [Boolean-function.00001010]
111. (and (or true A) (and B C)), [Boolean-function.00010001]
112. (and (or true A) (or B C)), [Boolean-function.01110111]
113. (and (or true A) (-> B C)), [Boolean-function.11011101]
114. (and (or true A) (<-> B C)), [Boolean-function.10011001]
115. (and (or A B) (or true C)), [Boolean-function.00111111]
116. (and (or A B) (or B C)), [Boolean-function.00110111]
117. (and (or A B) (-> A C)), [Boolean-function.00110101]
118. (and (or A B) (-> B C)), [Boolean-function.00011101]
119. (and (or A B) (-> C B)), [Boolean-function.00111011]
120. (and (or A B) (<-> A C)), [Boolean-function.00100101]
121. (and (or A B) (<-> B C)), [Boolean-function.00011001]
122. (and (-> A B) (or true C)), [Boolean-function.11110011]
123. (and (-> A B) (or A C)), [Boolean-function.01010011]
124. (and (-> A B) (or B C)), [Boolean-function.01110011]
125. (and (-> A B) (-> B C)), [Boolean-function.11010001]
126. (and (-> A B) (-> C A)), [Boolean-function.10100011]
127. (and (-> A B) (-> C B)), [Boolean-function.10110011]
128. (and (-> A B) (<-> A C)), [Boolean-function.10100001]
129. (and (-> A B) (<-> B C)), [Boolean-function.10010001]
130. (and (<-> A B) (or true C)), [Boolean-function.11000011]
131. (and (<-> A B) (or A C)), [Boolean-function.01000011]
132. (and (<-> A B) (-> A C)), [Boolean-function.11000001]
133. (and (<-> A B) (-> C A)), [Boolean-function.10000011]
134. (and (<-> A B) (<-> A C)), [Boolean-function.10000001]
135. (and (or true (and A B)) C), [Boolean-function.01010101]
136. (and (or A (and B C)) B), [Boolean-function.00010011]
137. (and (or A (or B C)) B), [Boolean-function.00110011]
138. (and (-> A (and nil B)) C), [Boolean-function.01010000]
139. (and (-> A (and B C)) B), [Boolean-function.00110001]
140. (and (<-> A (and B C)) B), [Boolean-function.00100001]
141. (and (<-> (and nil A) B) C), [Boolean-function.01000100]
142. (or true (and A (and B C))), [Boolean-function.11111111]
143. (or A (and (or true B) C)), [Boolean-function.01011111]
144. (or A (-> B (and nil C))), [Boolean-function.11001111]
145. (or A (<-> (and nil B) C)), [Boolean-function.10101111]
146. (or (and A B) (-> C B)), [Boolean-function.10111011]
147. (or (and A B) (<-> A C)), [Boolean-function.10100111]
148. (or (and A B) (<-> B C)), [Boolean-function.10011011]
149. (or (<-> A B) (and A C)), [Boolean-function.11000111]
150. (or (<-> A B) (and B C)), [Boolean-function.11010011]
151. (or (<-> A B) (<-> A C)), [Boolean-function.11100111]
152. (or (<-> A B) (<-> B C)), [Boolean-function.11011011]
153. (or (-> A (and nil B)) C), [Boolean-function.11110101]
154. (or (<-> A (or B C)) B), [Boolean-function.10110111]
155. (or (<-> A (<-> B C)) B), [Boolean-function.01111011]
156. (-> A (and nil (and B C))), [Boolean-function.11110000]
157. (-> A (-> B (and nil C))), [Boolean-function.11111100]
158. (-> A (<-> (and nil B) C)), [Boolean-function.11111010]
159. (-> (or A B) (and nil C)), [Boolean-function.11000000]
160. (-> (or A B) (and A C)), [Boolean-function.11000101]
161. (-> (or A B) (<-> A C)), [Boolean-function.11100101]
162. (-> (or A B) (<-> B C)), [Boolean-function.11011001]
163. (-> (-> A B) (<-> A C)), [Boolean-function.10101101]
164. (-> (-> A B) (<-> B C)), [Boolean-function.10011101]
165. (-> (<-> A B) (and nil C)), [Boolean-function.00111100]
166. (-> (<-> A B) (and A C)), [Boolean-function.00111101]
167. (-> (<-> A B) (<-> A C)), [Boolean-function.10111101]
168. (<-> A (and B (or A C))), [Boolean-function.11100011]
169. (<-> A (and (or true B) C)), [Boolean-function.10100101]
170. (<-> A (and (-> B A) C)), [Boolean-function.10110101]
171. (<-> A (and (<-> A B) C)), [Boolean-function.10110001]
172. (<-> A (or B (<-> A C))), [Boolean-function.01000111]
173. (<-> A (or (<-> A B) C)), [Boolean-function.00100111]
174. (<-> A (-> (-> B A) C)), [Boolean-function.10000101]
175. (<-> A (-> (<-> A B) C)), [Boolean-function.10001101]
176. (<-> A (<-> B (and A C))), [Boolean-function.00111001]
177. (<-> A (<-> B (or A C))), [Boolean-function.01100011]
178. (<-> A (<-> B (-> A C))), [Boolean-function.11001001]
179. (<-> A (<-> B (-> C A))), [Boolean-function.10010011]
180. (<-> A (<-> (and nil B) C)), [Boolean-function.01011010]
181. (<-> (and nil A) (and B C)), [Boolean-function.11101110]
182. (<-> (and nil A) (or B C)), [Boolean-function.10001000]
183. (<-> (and nil A) (-> B C)), [Boolean-function.00100010]
184. (<-> (and nil A) (<-> B C)), [Boolean-function.01100110]
185. (<-> (and A B) (and B C)), [Boolean-function.11101101]
186. (<-> (and A B) (or B C)), [Boolean-function.10001011]
187. (<-> (and nil (and A B)) C), [Boolean-function.10101010]
188. (<-> (and A (and B C)) B), [Boolean-function.11001101]
189. (<-> (and A (or B C)) B), [Boolean-function.11001011]
190. (<-> (or (<-> A B) C) B), [Boolean-function.00011011]
191. (<-> (-> A (and B C)) C), [Boolean-function.01011011]

---

Tortelvis.

What the Heck is Tortelvis?

Tortelvis is agile 130 kg strong Elvis impersonator singer of Dread Zeppelin,
the band that plays Led Zeppelin covers in a reggae style. Definitely
fascinating. But, sometimes, you do not want the copy, you want the real thing.
Look here:

> (set 'L (list 1 2 3))
(1 2 3)
> (set 'push-right (lambda(a b)(push a b -1)))
(lambda (a b) (push a b -1))
> (push-right 4 L)
(1 2 3 4)
> L
(1 2 3)

Did you expected (1 2 3 4)? Well, Newlisp is sometimes too functional. This
time it passed copy of L to the push-right. OK, we'll fix it now.

> (set 'push-right (lambda-macro(a b)(eval (expand '(push a b -1) 'a 'b))))
(lambda-macro (a b) (eval (expand '(push a b -1) 'a 'b)))
> (push-right 5 L)
(1 2 3 5)
> L
(1 2 3 5)

---

One Hundred Propositional Tautologies (5)

The same like last post, but this time 1500 tautologies, and
these are in the infix form. It is very easy to change prefix
into infix in Newlisp. And vice versa - same function can be
used for changing infix to prefix. But, tautologies are great.

(set 'infix<->prefix 
  (lambda(L)
    (cond ((symbol? L) L)
          ((= (length L) 2) (map infix<->prefix L))
          ((= (length L) 3) (let((L1 (map infix<->prefix L)))
                                (list (nth 1 L1) (nth 0 L1) (nth 2 L1)))))))

Generated 1005725 formulas.
Filtered to 187105 tautologies in T1.
Filtered to 2730 tautologies in T2.
Filtered to 1581 tautologies in T3 and 1149 tautologies in M3.

*** T3 ***

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

401. (not ((not a) <-> (a and true)))
402. (not ((not a) <-> (a and a)))
403. (not ((not a) <-> (false or a)))
404. (not ((not a) <-> (a or false)))
405. (not ((not a) <-> (a or a)))
406. (not ((not a) <-> (true -> a)))
407. (not ((not a) <-> (true <-> a)))
408. (not ((not a) <-> (a <-> true)))
409. (not ((true and a) <-> (not a)))
410. (not ((a and true) <-> (not a)))
411. (not ((a and a) <-> (not a)))
412. (not ((false or a) <-> (not a)))
413. (not ((a or false) <-> (not a)))
414. (not ((a or a) <-> (not a)))
415. (not ((true -> a) <-> (not a)))
416. (not ((true <-> a) <-> (not a)))
417. (not ((a <-> true) <-> (not a)))
418. (not ((not (not (not a))) <-> a))
419. (not ((not (true and a)) <-> a))
420. (not ((not (a and true)) <-> a))
421. (not ((not (a and a)) <-> a))
422. (not ((not (false or a)) <-> a))
423. (not ((not (a or false)) <-> a))
424. (not ((not (a or a)) <-> a))
425. (not ((not (true -> a)) <-> a))
426. (not ((not (true <-> a)) <-> a))
427. (not ((not (a <-> true)) <-> a))
428. (not ((true and (not a)) <-> a))
429. (not ((a and (not true)) <-> true))
430. (not ((a and (not a)) <-> true))
431. (not (((not true) and a) <-> true))
432. (not (((not a) and true) <-> a))
433. (not (((not a) and a) <-> true))
434. (not ((false or (not a)) <-> a))
435. (not (((not a) or false) <-> a))
436. (not ((true -> (not a)) <-> a))
437. (not ((a -> (not true)) <-> a))
438. (not ((a -> (not a)) <-> a))
439. (not ((true <-> (not a)) <-> a))
440. (not ((a <-> (not true)) <-> a))
441. (not ((a <-> (not a)) <-> true))
442. (not (((not true) <-> a) <-> a))
443. (not (((not a) <-> true) <-> a))
444. (not (((not a) <-> a) <-> true))
445. (a or (not (not (a -> b))))
446. (a or (not (not (false <-> a))))
447. (a or (not (not (a <-> false))))
448. (a or (not (a or (not true))))
449. (a or (not ((not true) or a)))
450. (a or (not ((not a) -> false)))
451. (a or (not ((not a) -> a)))
452. (a or (not (false <-> (not a))))
453. (a or (not ((not a) <-> false)))
454. (a or (true and (a -> b)))
455. (a or (true and (false <-> a)))
456. (a or (true and (a <-> false)))
457. (a or ((not a) and (not a)))
458. (a or ((a -> b) and true))
459. (a or ((false <-> a) and true))
460. (a or ((a <-> false) and true))
461. (a or (b or (a -> c)))
462. (a or (b or (false <-> a)))
463. (a or (b or (a <-> false)))
464. (a or (b or (a <-> b)))
465. (a or (b or (b <-> a)))
466. (a or ((a -> b) or c))
467. (a or ((false <-> a) or b))
468. (a or ((a <-> false) or b))
469. (a or ((a <-> b) or b))
470. (a or ((b <-> a) or b))
471. (a or (b -> (a -> c)))
472. (a or (b -> (false <-> a)))
473. (a or (b -> (a <-> false)))
474. (a or ((not (not a)) -> b))
475. (a or ((a and b) -> c))
476. (a or ((b and a) -> c))
477. (a or ((false or a) -> b))
478. (a or ((a or false) -> b))
479. (a or ((a or a) -> b))
480. (a or ((a or b) -> b))
481. (a or ((b or a) -> b))
482. (a or ((true -> a) -> b))
483. (a or ((true <-> a) -> b))
484. (a or ((a <-> true) -> b))
485. (a or (true <-> (a -> b)))
486. (a or (true <-> (false <-> a)))
487. (a or (true <-> (a <-> false)))
488. (a or (false <-> (not (not a))))
489. (a or (false <-> (a and b)))
490. (a or (false <-> (b and a)))
491. (a or (false <-> (a or a)))
492. (a or (false <-> (true -> a)))
493. (a or (false <-> (true <-> a)))
494. (a or (false <-> (a <-> true)))
495. (a or (a <-> (false and b)))
496. (a or (a <-> (a and b)))
497. (a or (a <-> (b and false)))
498. (a or (a <-> (b and a)))
499. (a or (a <-> (false or false)))
500. (a or (a <-> (true -> false)))
501. (a or (a <-> (true <-> false)))
502. (a or (a <-> (false <-> true)))
503. (a or (b <-> (a or b)))
504. (a or (b <-> (b or a)))
505. (a or ((not (not a)) <-> false))
506. (a or ((false and b) <-> a))
507. (a or ((a and b) <-> false))
508. (a or ((a and b) <-> a))
509. (a or ((b and false) <-> a))
510. (a or ((b and a) <-> false))
511. (a or ((b and a) <-> a))
512. (a or ((false or false) <-> a))
513. (a or ((a or a) <-> false))
514. (a or ((a or b) <-> b))
515. (a or ((b or a) <-> b))
516. (a or ((true -> false) <-> a))
517. (a or ((true -> a) <-> false))
518. (a or ((a -> b) <-> true))
519. (a or ((true <-> false) <-> a))
520. (a or ((true <-> a) <-> false))
521. (a or ((false <-> true) <-> a))
522. (a or ((false <-> a) <-> true))
523. (a or ((a <-> true) <-> false))
524. (a or ((a <-> false) <-> true))
525. ((not a) or (not (a -> false)))
526. ((not a) or (not (false <-> a)))
527. ((not a) or (not (a <-> false)))
528. ((not (not a)) or (a -> b))
529. ((not (not a)) or (false <-> a))
530. ((not (not a)) or (a <-> false))
531. ((true and a) or (a -> b))
532. ((true and a) or (false <-> a))
533. ((true and a) or (a <-> false))
534. ((a and true) or (a -> b))
535. ((a and true) or (false <-> a))
536. ((a and true) or (a <-> false))
537. ((a and a) or (a -> b))
538. ((a and a) or (false <-> a))
539. ((a and a) or (a <-> false))
540. ((a or b) or (a -> c))
541. ((a or b) or (b -> c))
542. ((a or b) or (false <-> a))
543. ((a or b) or (false <-> b))
544. ((a or b) or (a <-> false))
545. ((a or b) or (a <-> b))
546. ((a or b) or (b <-> false))
547. ((a or b) or (b <-> a))
548. ((a -> b) or (not (not a)))
549. ((a -> b) or (true and a))
550. ((a -> b) or (a and true))
551. ((a -> b) or (a and a))
552. ((a -> b) or (a or c))
553. ((a -> b) or (c or a))
554. ((a -> b) or (b -> c))
555. ((a -> b) or (c -> a))
556. ((a -> b) or (true <-> a))
557. ((a -> b) or (false <-> b))
558. ((a -> b) or (a <-> true))
559. ((a -> b) or (b <-> false))
560. ((true <-> a) or (a -> b))
561. ((true <-> a) or (false <-> a))
562. ((true <-> a) or (a <-> false))
563. ((false <-> a) or (not (not a)))
564. ((false <-> a) or (true and a))
565. ((false <-> a) or (a and true))
566. ((false <-> a) or (a and a))
567. ((false <-> a) or (a or b))
568. ((false <-> a) or (b or a))
569. ((false <-> a) or (b -> a))
570. ((false <-> a) or (true <-> a))
571. ((false <-> a) or (a <-> true))
572. ((a <-> true) or (a -> b))
573. ((a <-> true) or (false <-> a))
574. ((a <-> true) or (a <-> false))
575. ((a <-> false) or (not (not a)))
576. ((a <-> false) or (true and a))
577. ((a <-> false) or (a and true))
578. ((a <-> false) or (a and a))
579. ((a <-> false) or (a or b))
580. ((a <-> false) or (b or a))
581. ((a <-> false) or (b -> a))
582. ((a <-> false) or (true <-> a))
583. ((a <-> false) or (a <-> true))
584. ((a <-> b) or (a or b))
585. ((a <-> b) or (b or a))
586. ((not (a -> false)) or (not a))
587. ((not (false <-> a)) or (not a))
588. ((not (a <-> false)) or (not a))
589. ((not (not (a -> b))) or a)
590. ((not (not (false <-> a))) or a)
591. ((not (not (a <-> false))) or a)
592. ((not (a or (not true))) or a)
593. ((not ((not true) or a)) or a)
594. ((not ((not a) -> false)) or a)
595. ((not ((not a) -> a)) or a)
596. ((not (false <-> (not a))) or a)
597. ((not ((not a) <-> false)) or a)
598. ((true and (a -> b)) or a)
599. ((true and (false <-> a)) or a)
600. ((true and (a <-> false)) or a)
601. (((not a) and (not a)) or a)
602. (((a -> b) and true) or a)
603. (((false <-> a) and true) or a)
604. (((a <-> false) and true) or a)
605. ((a or (b -> c)) or b)
606. ((a or (false <-> b)) or b)
607. ((a or (a <-> b)) or b)
608. ((a or (b <-> false)) or b)
609. ((a or (b <-> a)) or b)
610. (((a -> b) or c) or a)
611. (((false <-> a) or b) or a)
612. (((a <-> false) or b) or a)
613. (((a <-> b) or a) or b)
614. (((a <-> b) or b) or a)
615. ((a -> (b -> c)) or b)
616. ((a -> (false <-> b)) or b)
617. ((a -> (b <-> false)) or b)
618. (((not (not a)) -> b) or a)
619. (((a and b) -> c) or a)
620. (((a and b) -> c) or b)
621. (((false or a) -> b) or a)
622. (((a or false) -> b) or a)
623. (((a or a) -> b) or a)
624. (((a or b) -> a) or b)
625. (((a or b) -> b) or a)
626. (((true -> a) -> b) or a)
627. (((true <-> a) -> b) or a)
628. (((a <-> true) -> b) or a)
629. ((true <-> (a -> b)) or a)
630. ((true <-> (false <-> a)) or a)
631. ((true <-> (a <-> false)) or a)
632. ((false <-> (not (not a))) or a)
633. ((false <-> (a and b)) or a)
634. ((false <-> (a and b)) or b)
635. ((false <-> (a or a)) or a)
636. ((false <-> (true -> a)) or a)
637. ((false <-> (true <-> a)) or a)
638. ((false <-> (a <-> true)) or a)
639. ((a <-> (false and b)) or a)
640. ((a <-> (a and b)) or a)
641. ((a <-> (b and false)) or a)
642. ((a <-> (b and a)) or a)
643. ((a <-> (false or false)) or a)
644. ((a <-> (a or b)) or b)
645. ((a <-> (b or a)) or b)
646. ((a <-> (true -> false)) or a)
647. ((a <-> (true <-> false)) or a)
648. ((a <-> (false <-> true)) or a)
649. (((not (not a)) <-> false) or a)
650. (((false and a) <-> b) or b)
651. (((a and false) <-> b) or b)
652. (((a and b) <-> false) or a)
653. (((a and b) <-> false) or b)
654. (((a and b) <-> a) or a)
655. (((a and b) <-> b) or b)
656. (((false or false) <-> a) or a)
657. (((a or a) <-> false) or a)
658. (((a or b) <-> a) or b)
659. (((a or b) <-> b) or a)
660. (((true -> false) <-> a) or a)
661. (((true -> a) <-> false) or a)
662. (((a -> b) <-> true) or a)
663. (((true <-> false) <-> a) or a)
664. (((true <-> a) <-> false) or a)
665. (((false <-> true) <-> a) or a)
666. (((false <-> a) <-> true) or a)
667. (((a <-> true) <-> false) or a)
668. (((a <-> false) <-> true) or a)
669. (a -> (not (not (not (not a)))))
670. (a -> (not (not (true and a))))
671. (a -> (not (not (a and true))))
672. (a -> (not (not (a and a))))
673. (a -> (not (not (a or b))))
674. (a -> (not (not (b or a))))
675. (a -> (not (not (b -> a))))
676. (a -> (not (not (true <-> a))))
677. (a -> (not (not (a <-> true))))
678. (a -> (not (b and (not a))))
679. (a -> (not ((not a) and b)))
680. (a -> (not (false or (not a))))
681. (a -> (not ((not a) or false)))
682. (a -> (not (true -> (not a))))
683. (a -> (not (a -> (not true))))
684. (a -> (not (a -> (not a))))
685. (a -> (not (true <-> (not a))))
686. (a -> (not (a <-> (not true))))
687. (a -> (not ((not true) <-> a)))
688. (a -> (not ((not a) <-> true)))
689. (a -> (true and (not (not a))))
690. (a -> (true and (true and a)))
691. (a -> (true and (a and true)))
692. (a -> (true and (a and a)))
693. (a -> (true and (a or b)))
694. (a -> (true and (b or a)))
695. (a -> (true and (b -> a)))
696. (a -> (true and (true <-> a)))
697. (a -> (true and (a <-> true)))
698. (a -> (a and (not (not a))))
699. (a -> (a and (true and a)))
700. (a -> (a and (a and true)))
701. (a -> (a and (a and a)))
702. (a -> (a and (a or b)))
703. (a -> (a and (b or a)))
704. (a -> (a and (b -> a)))
705. (a -> (a and (true <-> a)))
706. (a -> (a and (a <-> true)))
707. (a -> ((not (not a)) and true))
708. (a -> ((not (not a)) and a))
709. (a -> ((true and a) and true))
710. (a -> ((true and a) and a))
711. (a -> ((a and true) and true))
712. (a -> ((a and true) and a))
713. (a -> ((a and a) and true))
714. (a -> ((a and a) and a))
715. (a -> ((a or b) and true))
716. (a -> ((a or b) and a))
717. (a -> ((b or a) and true))
718. (a -> ((b or a) and a))
719. (a -> ((b -> a) and true))
720. (a -> ((b -> a) and a))
721. (a -> ((true <-> a) and true))
722. (a -> ((true <-> a) and a))
723. (a -> ((a <-> true) and true))
724. (a -> ((a <-> true) and a))
725. (a -> (b or (not (not a))))
726. (a -> (b or (true and a)))
727. (a -> (b or (a and true)))
728. (a -> (b or (a and a)))
729. (a -> (b or (a or c)))
730. (a -> (b or (c or a)))
731. (a -> (b or (c -> a)))
732. (a -> (b or (true <-> a)))
733. (a -> (b or (a <-> true)))
734. (a -> ((not (not a)) or b))
735. (a -> ((true and a) or b))
736. (a -> ((a and true) or b))
737. (a -> ((a and a) or b))
738. (a -> ((a or b) or c))
739. (a -> ((b or a) or c))
740. (a -> ((b -> a) or c))
741. (a -> ((true <-> a) or b))
742. (a -> ((a <-> true) or b))
743. (a -> (b -> (not (not a))))
744. (a -> (b -> (true and a)))
745. (a -> (b -> (a and true)))
746. (a -> (b -> (a and a)))
747. (a -> (b -> (a and b)))
748. (a -> (b -> (b and a)))
749. (a -> (b -> (a or c)))
750. (a -> (b -> (c or a)))
751. (a -> (b -> (c -> a)))
752. (a -> (b -> (true <-> a)))
753. (a -> (b -> (a <-> true)))
754. (a -> (b -> (a <-> b)))
755. (a -> (b -> (b <-> a)))
756. (a -> ((a -> false) -> b))
757. (a -> ((a -> b) -> b))
758. (a -> ((false <-> a) -> b))
759. (a -> ((a <-> false) -> b))
760. (a -> ((a <-> b) -> b))
761. (a -> ((b <-> a) -> b))
762. (a -> (true <-> (not (not a))))
763. (a -> (true <-> (a and a)))
764. (a -> (true <-> (a or b)))
765. (a -> (true <-> (b or a)))
766. (a -> (true <-> (b -> a)))
767. (a -> (a <-> (a or b)))
768. (a -> (a <-> (b or a)))
769. (a -> (a <-> (b -> a)))
770. (a -> (b <-> (a and b)))
771. (a -> (b <-> (b and a)))
772. (a -> (b <-> (a -> b)))
773. (a -> (b <-> (a <-> b)))
774. (a -> (b <-> (b <-> a)))
775. (a -> ((not true) <-> (not a)))
776. (a -> ((not a) <-> (not true)))
777. (a -> ((not (not a)) <-> true))
778. (a -> ((a and a) <-> true))
779. (a -> ((a and b) <-> b))
780. (a -> ((b and a) <-> b))
781. (a -> ((a or b) <-> true))
782. (a -> ((a or b) <-> a))
783. (a -> ((b or a) <-> true))
784. (a -> ((b or a) <-> a))
785. (a -> ((a -> b) <-> b))
786. (a -> ((b -> a) <-> true))
787. (a -> ((b -> a) <-> a))
788. (a -> ((a <-> b) <-> b))
789. (a -> ((b <-> a) <-> b))
790. ((not a) -> (not (a and b)))
791. ((not a) -> (not (b and a)))
792. ((not a) -> (not (false or a)))
793. ((not a) -> (not (a or false)))
794. ((not a) -> (not (a or a)))
795. ((not a) -> (not (true -> a)))
796. ((not a) -> (not (true <-> a)))
797. ((not a) -> (not (a <-> true)))
798. ((not a) -> (a <-> (not true)))
799. ((not a) -> ((not true) <-> a))
800. ((not (not a)) -> (true and a))

801. ((not (not a)) -> (a and true))
802. ((not (not a)) -> (a and a))
803. ((not (not a)) -> (a or b))
804. ((not (not a)) -> (b or a))
805. ((not (not a)) -> (b -> a))
806. ((not (not a)) -> (true <-> a))
807. ((not (not a)) -> (a <-> true))
808. ((a and b) -> (not (not a)))
809. ((a and b) -> (not (not b)))
810. ((a and b) -> (true and a))
811. ((a and b) -> (true and b))
812. ((a and b) -> (a and true))
813. ((a and b) -> (a and a))
814. ((a and b) -> (b and true))
815. ((a and b) -> (b and a))
816. ((a and b) -> (b and b))
817. ((a and b) -> (a or c))
818. ((a and b) -> (b or c))
819. ((a and b) -> (c or a))
820. ((a and b) -> (c or b))
821. ((a and b) -> (c -> a))
822. ((a and b) -> (c -> b))
823. ((a and b) -> (true <-> a))
824. ((a and b) -> (true <-> b))
825. ((a and b) -> (a <-> true))
826. ((a and b) -> (a <-> b))
827. ((a and b) -> (b <-> true))
828. ((a and b) -> (b <-> a))
829. ((false or a) -> (not (not a)))
830. ((false or a) -> (true and a))
831. ((false or a) -> (a and true))
832. ((false or a) -> (a and a))
833. ((false or a) -> (a or b))
834. ((false or a) -> (b or a))
835. ((false or a) -> (b -> a))
836. ((false or a) -> (true <-> a))
837. ((false or a) -> (a <-> true))
838. ((a or false) -> (not (not a)))
839. ((a or false) -> (true and a))
840. ((a or false) -> (a and true))
841. ((a or false) -> (a and a))
842. ((a or false) -> (a or b))
843. ((a or false) -> (b or a))
844. ((a or false) -> (b -> a))
845. ((a or false) -> (true <-> a))
846. ((a or false) -> (a <-> true))
847. ((a or a) -> (not (not a)))
848. ((a or a) -> (true and a))
849. ((a or a) -> (a and true))
850. ((a or a) -> (a and a))
851. ((a or a) -> (a or b))
852. ((a or a) -> (b or a))
853. ((a or a) -> (b -> a))
854. ((a or a) -> (true <-> a))
855. ((a or a) -> (a <-> true))
856. ((a or b) -> (b or a))
857. ((true -> a) -> (not (not a)))
858. ((true -> a) -> (true and a))
859. ((true -> a) -> (a and true))
860. ((true -> a) -> (a and a))
861. ((true -> a) -> (a or b))
862. ((true -> a) -> (b or a))
863. ((true -> a) -> (b -> a))
864. ((true -> a) -> (true <-> a))
865. ((true -> a) -> (a <-> true))
866. ((a -> false) -> (a -> b))
867. ((a -> false) -> (false <-> a))
868. ((a -> false) -> (a <-> false))
869. ((true <-> a) -> (not (not a)))
870. ((true <-> a) -> (true and a))
871. ((true <-> a) -> (a and true))
872. ((true <-> a) -> (a and a))
873. ((true <-> a) -> (a or b))
874. ((true <-> a) -> (b or a))
875. ((true <-> a) -> (b -> a))
876. ((false <-> a) -> (a -> b))
877. ((a <-> true) -> (not (not a)))
878. ((a <-> true) -> (true and a))
879. ((a <-> true) -> (a and true))
880. ((a <-> true) -> (a and a))
881. ((a <-> true) -> (a or b))
882. ((a <-> true) -> (b or a))
883. ((a <-> true) -> (b -> a))
884. ((a <-> false) -> (a -> b))
885. ((a <-> b) -> (a -> b))
886. ((a <-> b) -> (b -> a))
887. ((a <-> b) -> (b <-> a))
888. ((not (true and a)) -> (not a))
889. ((not (a and true)) -> (not a))
890. ((not (a and a)) -> (not a))
891. ((not (a or b)) -> (not a))
892. ((not (a or b)) -> (not b))
893. ((not (a -> b)) -> (not b))
894. ((not (true <-> a)) -> (not a))
895. ((not (a <-> true)) -> (not a))
896. ((a -> (not true)) -> (not a))
897. ((a -> (not a)) -> (not a))
898. ((a <-> (not true)) -> (not a))
899. (((not true) <-> a) -> (not a))
900. ((not (not (not (not a)))) -> a)
901. ((not (not (a and b))) -> a)
902. ((not (not (a and b))) -> b)
903. ((not (not (false or a))) -> a)
904. ((not (not (a or false))) -> a)
905. ((not (not (a or a))) -> a)
906. ((not (not (true -> a))) -> a)
907. ((not (not (true <-> a))) -> a)
908. ((not (not (a <-> true))) -> a)
909. ((not (true and (not a))) -> a)
910. ((not ((not a) and true)) -> a)
911. ((not (a or (not b))) -> b)
912. ((not ((not a) or b)) -> a)
913. ((not (a -> (not b))) -> b)
914. ((not (true <-> (not a))) -> a)
915. ((not (a <-> (not true))) -> a)
916. ((not ((not true) <-> a)) -> a)
917. ((not ((not a) <-> true)) -> a)
918. ((a and (not (not b))) -> b)
919. ((a and (false and b)) -> c)
920. ((a and (b and false)) -> c)
921. ((a and (b and c)) -> b)
922. ((a and (b and c)) -> c)
923. ((a and (false or false)) -> b)
924. ((a and (false or b)) -> b)
925. ((a and (b or false)) -> b)
926. ((a and (b or b)) -> b)
927. ((a and (true -> false)) -> b)
928. ((a and (true -> b)) -> b)
929. ((a and (a -> false)) -> b)
930. ((a and (a -> b)) -> b)
931. ((a and (true <-> false)) -> b)
932. ((a and (true <-> b)) -> b)
933. ((a and (false <-> true)) -> b)
934. ((a and (false <-> a)) -> b)
935. ((a and (a <-> false)) -> b)
936. ((a and (a <-> b)) -> b)
937. ((a and (b <-> true)) -> b)
938. ((a and (b <-> a)) -> b)
939. (((not (not a)) and b) -> a)
940. (((false and a) and b) -> c)
941. (((a and false) and b) -> c)
942. (((a and b) and c) -> a)
943. (((a and b) and c) -> b)
944. (((false or false) and a) -> b)
945. (((false or a) and b) -> a)
946. (((a or false) and b) -> a)
947. (((a or a) and b) -> a)
948. (((true -> false) and a) -> b)
949. (((true -> a) and b) -> a)
950. (((a -> false) and a) -> b)
951. (((a -> b) and a) -> b)
952. (((true <-> false) and a) -> b)
953. (((true <-> a) and b) -> a)
954. (((false <-> true) and a) -> b)
955. (((false <-> a) and a) -> b)
956. (((a <-> true) and b) -> a)
957. (((a <-> false) and a) -> b)
958. (((a <-> b) and a) -> b)
959. (((a <-> b) and b) -> a)
960. ((false or (not (not a))) -> a)
961. ((false or (false and a)) -> b)
962. ((false or (a and false)) -> b)
963. ((false or (a and b)) -> a)
964. ((false or (a and b)) -> b)
965. ((false or (false or false)) -> a)
966. ((false or (false or a)) -> a)
967. ((false or (a or false)) -> a)
968. ((false or (a or a)) -> a)
969. ((false or (true -> false)) -> a)
970. ((false or (true -> a)) -> a)
971. ((false or (true <-> false)) -> a)
972. ((false or (true <-> a)) -> a)
973. ((false or (false <-> true)) -> a)
974. ((false or (a <-> true)) -> a)
975. ((a or (not (not a))) -> a)
976. ((a or (false and b)) -> a)
977. ((a or (a and b)) -> a)
978. ((a or (b and false)) -> a)
979. ((a or (b and a)) -> a)
980. ((a or (false or false)) -> a)
981. ((a or (false or a)) -> a)
982. ((a or (a or false)) -> a)
983. ((a or (a or a)) -> a)
984. ((a or (true -> false)) -> a)
985. ((a or (true -> a)) -> a)
986. ((a or (true <-> false)) -> a)
987. ((a or (true <-> a)) -> a)
988. ((a or (false <-> true)) -> a)
989. ((a or (a <-> true)) -> a)
990. (((not true) or (not true)) -> a)
991. (((not (not a)) or false) -> a)
992. (((not (not a)) or a) -> a)
993. (((false and a) or false) -> b)
994. (((false and a) or b) -> b)
995. (((a and false) or false) -> b)
996. (((a and false) or b) -> b)
997. (((a and b) or false) -> a)
998. (((a and b) or false) -> b)
999. (((a and b) or a) -> a)
1000. (((a and b) or b) -> b)
1001. (((false or false) or false) -> a)
1002. (((false or false) or a) -> a)
1003. (((false or a) or false) -> a)
1004. (((false or a) or a) -> a)
1005. (((a or false) or false) -> a)
1006. (((a or false) or a) -> a)
1007. (((a or a) or false) -> a)
1008. (((a or a) or a) -> a)
1009. (((true -> false) or false) -> a)
1010. (((true -> false) or a) -> a)
1011. (((true -> a) or false) -> a)
1012. (((true -> a) or a) -> a)
1013. (((true <-> false) or false) -> a)
1014. (((true <-> false) or a) -> a)
1015. (((true <-> a) or false) -> a)
1016. (((true <-> a) or a) -> a)
1017. (((false <-> true) or false) -> a)
1018. (((false <-> true) or a) -> a)
1019. (((a <-> true) or false) -> a)
1020. (((a <-> true) or a) -> a)
1021. ((true -> (not (not a))) -> a)
1022. ((true -> (false and a)) -> b)
1023. ((true -> (a and false)) -> b)
1024. ((true -> (a and b)) -> a)
1025. ((true -> (a and b)) -> b)
1026. ((true -> (false or false)) -> a)
1027. ((true -> (false or a)) -> a)
1028. ((true -> (a or false)) -> a)
1029. ((true -> (a or a)) -> a)
1030. ((true -> (true -> false)) -> a)
1031. ((true -> (true -> a)) -> a)
1032. ((true -> (true <-> false)) -> a)
1033. ((true -> (true <-> a)) -> a)
1034. ((true -> (false <-> true)) -> a)
1035. ((true -> (a <-> true)) -> a)
1036. (((not a) -> (not true)) -> a)
1037. (((a -> b) -> false) -> a)
1038. (((a -> b) -> a) -> a)
1039. (((false <-> a) -> false) -> a)
1040. (((false <-> a) -> a) -> a)
1041. (((a <-> false) -> false) -> a)
1042. (((a <-> false) -> a) -> a)
1043. ((true <-> (not (not a))) -> a)
1044. ((true <-> (false and a)) -> b)
1045. ((true <-> (a and false)) -> b)
1046. ((true <-> (a and b)) -> a)
1047. ((true <-> (a and b)) -> b)
1048. ((true <-> (false or false)) -> a)
1049. ((true <-> (false or a)) -> a)
1050. ((true <-> (a or false)) -> a)
1051. ((true <-> (a or a)) -> a)
1052. ((false <-> (a -> b)) -> a)
1053. ((a <-> (a -> false)) -> b)
1054. ((a <-> (a -> b)) -> a)
1055. ((a <-> (a -> b)) -> b)
1056. ((a <-> (false <-> a)) -> b)
1057. ((a <-> (a <-> false)) -> b)
1058. ((a <-> (a <-> b)) -> b)
1059. ((a <-> (b <-> a)) -> b)
1060. (((not true) <-> (not a)) -> a)
1061. (((not a) <-> (not true)) -> a)
1062. (((not (not a)) <-> true) -> a)
1063. (((false and a) <-> true) -> b)
1064. (((a and false) <-> true) -> b)
1065. (((a and b) <-> true) -> a)
1066. (((a and b) <-> true) -> b)
1067. (((false or false) <-> true) -> a)
1068. (((false or a) <-> true) -> a)
1069. (((a or false) <-> true) -> a)
1070. (((a or a) <-> true) -> a)
1071. (((a -> false) <-> a) -> b)
1072. (((a -> b) <-> false) -> a)
1073. (((a -> b) <-> a) -> a)
1074. (((a -> b) <-> a) -> b)
1075. (((false <-> a) <-> a) -> b)
1076. (((a <-> false) <-> a) -> b)
1077. (((a <-> b) <-> a) -> b)
1078. (((a <-> b) <-> b) -> a)
1079. (false <-> (a and (false and b)))
1080. (false <-> (a and (b and false)))
1081. (false <-> (a and (false or false)))
1082. (false <-> (a and (true -> false)))
1083. (false <-> (a and (a -> false)))
1084. (false <-> (a and (true <-> false)))
1085. (false <-> (a and (false <-> true)))
1086. (false <-> (a and (false <-> a)))
1087. (false <-> (a and (a <-> false)))
1088. (false <-> ((false and a) and b))
1089. (false <-> ((a and false) and b))
1090. (false <-> ((false or false) and a))
1091. (false <-> ((true -> false) and a))
1092. (false <-> ((a -> false) and a))
1093. (false <-> ((true <-> false) and a))
1094. (false <-> ((false <-> true) and a))
1095. (false <-> ((false <-> a) and a))
1096. (false <-> ((a <-> false) and a))
1097. (false <-> ((not true) or (not true)))
1098. (false <-> (true -> (false and a)))
1099. (false <-> (true -> (a and false)))
1100. (false <-> (true <-> (false and a)))
1101. (false <-> (true <-> (a and false)))
1102. (false <-> (a <-> (a -> false)))
1103. (false <-> ((false and a) <-> true))
1104. (false <-> ((a and false) <-> true))
1105. (false <-> ((a -> false) <-> a))
1106. (a <-> (not (not (not (not a)))))
1107. (a <-> (not (not (true and a))))
1108. (a <-> (not (not (a and true))))
1109. (a <-> (not (not (a and a))))
1110. (a <-> (not (not (false or a))))
1111. (a <-> (not (not (a or false))))
1112. (a <-> (not (not (a or a))))
1113. (a <-> (not (not (true -> a))))
1114. (a <-> (not (not (true <-> a))))
1115. (a <-> (not (not (a <-> true))))
1116. (a <-> (not (true and (not a))))
1117. (a <-> (not ((not a) and true)))
1118. (a <-> (not (false or (not a))))
1119. (a <-> (not ((not a) or false)))
1120. (a <-> (not (true -> (not a))))
1121. (a <-> (not (a -> (not true))))
1122. (a <-> (not (a -> (not a))))
1123. (a <-> (not (true <-> (not a))))
1124. (a <-> (not (a <-> (not true))))
1125. (a <-> (not ((not true) <-> a)))
1126. (a <-> (not ((not a) <-> true)))
1127. (a <-> (true and (not (not a))))
1128. (a <-> (true and (true and a)))
1129. (a <-> (true and (a and true)))
1130. (a <-> (true and (a and a)))
1131. (a <-> (true and (false or a)))
1132. (a <-> (true and (a or false)))
1133. (a <-> (true and (a or a)))
1134. (a <-> (true and (true -> a)))
1135. (a <-> (true and (true <-> a)))
1136. (a <-> (true and (a <-> true)))
1137. (a <-> (a and (not (not a))))
1138. (a <-> (a and (true and a)))
1139. (a <-> (a and (a and true)))
1140. (a <-> (a and (a and a)))
1141. (a <-> (a and (a or b)))
1142. (a <-> (a and (b or a)))
1143. (a <-> (a and (b -> a)))
1144. (a <-> (a and (true <-> a)))
1145. (a <-> (a and (a <-> true)))
1146. (a <-> ((not (not a)) and true))
1147. (a <-> ((not (not a)) and a))
1148. (a <-> ((true and a) and true))
1149. (a <-> ((true and a) and a))
1150. (a <-> ((a and true) and true))
1151. (a <-> ((a and true) and a))
1152. (a <-> ((a and a) and true))
1153. (a <-> ((a and a) and a))
1154. (a <-> ((false or a) and true))
1155. (a <-> ((a or false) and true))
1156. (a <-> ((a or a) and true))
1157. (a <-> ((a or b) and a))
1158. (a <-> ((b or a) and a))
1159. (a <-> ((true -> a) and true))
1160. (a <-> ((b -> a) and a))
1161. (a <-> ((true <-> a) and true))
1162. (a <-> ((true <-> a) and a))
1163. (a <-> ((a <-> true) and true))
1164. (a <-> ((a <-> true) and a))
1165. (a <-> (false or (not (not a))))
1166. (a <-> (false or (true and a)))
1167. (a <-> (false or (a and true)))
1168. (a <-> (false or (a and a)))
1169. (a <-> (false or (false or a)))
1170. (a <-> (false or (a or false)))
1171. (a <-> (false or (a or a)))
1172. (a <-> (false or (true -> a)))
1173. (a <-> (false or (true <-> a)))
1174. (a <-> (false or (a <-> true)))
1175. (a <-> (a or (not (not a))))
1176. (a <-> (a or (false and b)))
1177. (a <-> (a or (a and b)))
1178. (a <-> (a or (b and false)))
1179. (a <-> (a or (b and a)))
1180. (a <-> (a or (false or false)))
1181. (a <-> (a or (false or a)))
1182. (a <-> (a or (a or false)))
1183. (a <-> (a or (a or a)))
1184. (a <-> (a or (true -> false)))
1185. (a <-> (a or (true -> a)))
1186. (a <-> (a or (true <-> false)))
1187. (a <-> (a or (true <-> a)))
1188. (a <-> (a or (false <-> true)))
1189. (a <-> (a or (a <-> true)))
1190. (a <-> ((not (not a)) or false))
1191. (a <-> ((not (not a)) or a))
1192. (a <-> ((true and a) or false))
1193. (a <-> ((false and b) or a))
1194. (a <-> ((a and true) or false))
1195. (a <-> ((a and a) or false))
1196. (a <-> ((a and b) or a))
1197. (a <-> ((b and false) or a))
1198. (a <-> ((b and a) or a))
1199. (a <-> ((false or false) or a))
1200. (a <-> ((false or a) or false))

1201. (a <-> ((false or a) or a))
1202. (a <-> ((a or false) or false))
1203. (a <-> ((a or false) or a))
1204. (a <-> ((a or a) or false))
1205. (a <-> ((a or a) or a))
1206. (a <-> ((true -> false) or a))
1207. (a <-> ((true -> a) or false))
1208. (a <-> ((true -> a) or a))
1209. (a <-> ((true <-> false) or a))
1210. (a <-> ((true <-> a) or false))
1211. (a <-> ((true <-> a) or a))
1212. (a <-> ((false <-> true) or a))
1213. (a <-> ((a <-> true) or false))
1214. (a <-> ((a <-> true) or a))
1215. (a <-> (true -> (not (not a))))
1216. (a <-> (true -> (true and a)))
1217. (a <-> (true -> (a and true)))
1218. (a <-> (true -> (a and a)))
1219. (a <-> (true -> (false or a)))
1220. (a <-> (true -> (a or false)))
1221. (a <-> (true -> (a or a)))
1222. (a <-> (true -> (true -> a)))
1223. (a <-> (true -> (true <-> a)))
1224. (a <-> (true -> (a <-> true)))
1225. (a <-> ((not a) -> (not true)))
1226. (a <-> ((a -> false) -> false))
1227. (a <-> ((a -> b) -> a))
1228. (a <-> ((false <-> a) -> false))
1229. (a <-> ((false <-> a) -> a))
1230. (a <-> ((a <-> false) -> false))
1231. (a <-> ((a <-> false) -> a))
1232. (a <-> (true <-> (not (not a))))
1233. (a <-> (true <-> (true and a)))
1234. (a <-> (true <-> (a and true)))
1235. (a <-> (true <-> (a and a)))
1236. (a <-> (true <-> (false or a)))
1237. (a <-> (true <-> (a or false)))
1238. (a <-> (true <-> (a or a)))
1239. (a <-> (true <-> (true -> a)))
1240. (a <-> (false <-> (a -> false)))
1241. (a <-> (b <-> (a <-> b)))
1242. (a <-> (b <-> (b <-> a)))
1243. (a <-> ((not true) <-> (not a)))
1244. (a <-> ((not a) <-> (not true)))
1245. (a <-> ((not (not a)) <-> true))
1246. (a <-> ((true and a) <-> true))
1247. (a <-> ((a and true) <-> true))
1248. (a <-> ((a and a) <-> true))
1249. (a <-> ((false or a) <-> true))
1250. (a <-> ((a or false) <-> true))
1251. (a <-> ((a or a) <-> true))
1252. (a <-> ((true -> a) <-> true))
1253. (a <-> ((a -> false) <-> false))
1254. (a <-> ((a <-> b) <-> b))
1255. (a <-> ((b <-> a) <-> b))
1256. ((not true) <-> (a and (not true)))
1257. ((not true) <-> (a and (not a)))
1258. ((not true) <-> ((not true) and a))
1259. ((not true) <-> ((not a) and a))
1260. ((not true) <-> (a <-> (not a)))
1261. ((not true) <-> ((not a) <-> a))
1262. ((not a) <-> (not (true and a)))
1263. ((not a) <-> (not (a and true)))
1264. ((not a) <-> (not (a and a)))
1265. ((not a) <-> (not (false or a)))
1266. ((not a) <-> (not (a or false)))
1267. ((not a) <-> (not (a or a)))
1268. ((not a) <-> (not (true -> a)))
1269. ((not a) <-> (not (true <-> a)))
1270. ((not a) <-> (not (a <-> true)))
1271. ((not a) <-> (a -> (not true)))
1272. ((not a) <-> (a -> (not a)))
1273. ((not a) <-> (a <-> (not true)))
1274. ((not a) <-> ((not true) <-> a))
1275. ((not (not a)) <-> (true and a))
1276. ((not (not a)) <-> (a and true))
1277. ((not (not a)) <-> (a and a))
1278. ((not (not a)) <-> (false or a))
1279. ((not (not a)) <-> (a or false))
1280. ((not (not a)) <-> (a or a))
1281. ((not (not a)) <-> (true -> a))
1282. ((not (not a)) <-> (true <-> a))
1283. ((not (not a)) <-> (a <-> true))
1284. ((true and a) <-> (not (not a)))
1285. ((true and a) <-> (a and a))
1286. ((true and a) <-> (false or a))
1287. ((true and a) <-> (a or false))
1288. ((true and a) <-> (a or a))
1289. ((true and a) <-> (true -> a))
1290. ((true and a) <-> (true <-> a))
1291. ((true and a) <-> (a <-> true))
1292. ((false and a) <-> (false and b))
1293. ((false and a) <-> (b and false))
1294. ((false and a) <-> (false or false))
1295. ((false and a) <-> (true -> false))
1296. ((false and a) <-> (true <-> false))
1297. ((false and a) <-> (false <-> true))
1298. ((a and true) <-> (not (not a)))
1299. ((a and true) <-> (a and a))
1300. ((a and true) <-> (false or a))
1301. ((a and true) <-> (a or false))
1302. ((a and true) <-> (a or a))
1303. ((a and true) <-> (true -> a))
1304. ((a and true) <-> (true <-> a))
1305. ((a and true) <-> (a <-> true))
1306. ((a and false) <-> (false and b))
1307. ((a and false) <-> (b and false))
1308. ((a and false) <-> (false or false))
1309. ((a and false) <-> (true -> false))
1310. ((a and false) <-> (true <-> false))
1311. ((a and false) <-> (false <-> true))
1312. ((a and a) <-> (not (not a)))
1313. ((a and a) <-> (true and a))
1314. ((a and a) <-> (a and true))
1315. ((a and a) <-> (false or a))
1316. ((a and a) <-> (a or false))
1317. ((a and a) <-> (a or a))
1318. ((a and a) <-> (true -> a))
1319. ((a and a) <-> (true <-> a))
1320. ((a and a) <-> (a <-> true))
1321. ((a and b) <-> (b and a))
1322. ((false or false) <-> (false and a))
1323. ((false or false) <-> (a and false))
1324. ((false or a) <-> (not (not a)))
1325. ((false or a) <-> (true and a))
1326. ((false or a) <-> (a and true))
1327. ((false or a) <-> (a and a))
1328. ((false or a) <-> (a or a))
1329. ((false or a) <-> (true -> a))
1330. ((false or a) <-> (true <-> a))
1331. ((false or a) <-> (a <-> true))
1332. ((a or false) <-> (not (not a)))
1333. ((a or false) <-> (true and a))
1334. ((a or false) <-> (a and true))
1335. ((a or false) <-> (a and a))
1336. ((a or false) <-> (a or a))
1337. ((a or false) <-> (true -> a))
1338. ((a or false) <-> (true <-> a))
1339. ((a or false) <-> (a <-> true))
1340. ((a or a) <-> (not (not a)))
1341. ((a or a) <-> (true and a))
1342. ((a or a) <-> (a and true))
1343. ((a or a) <-> (a and a))
1344. ((a or a) <-> (false or a))
1345. ((a or a) <-> (a or false))
1346. ((a or a) <-> (true -> a))
1347. ((a or a) <-> (true <-> a))
1348. ((a or a) <-> (a <-> true))
1349. ((a or b) <-> (b or a))
1350. ((true -> false) <-> (false and a))
1351. ((true -> false) <-> (a and false))
1352. ((true -> a) <-> (not (not a)))
1353. ((true -> a) <-> (true and a))
1354. ((true -> a) <-> (a and true))
1355. ((true -> a) <-> (a and a))
1356. ((true -> a) <-> (false or a))
1357. ((true -> a) <-> (a or false))
1358. ((true -> a) <-> (a or a))
1359. ((true -> a) <-> (true <-> a))
1360. ((true -> a) <-> (a <-> true))
1361. ((a -> false) <-> (false <-> a))
1362. ((a -> false) <-> (a <-> false))
1363. ((true <-> false) <-> (false and a))
1364. ((true <-> false) <-> (a and false))
1365. ((true <-> a) <-> (not (not a)))
1366. ((true <-> a) <-> (true and a))
1367. ((true <-> a) <-> (a and true))
1368. ((true <-> a) <-> (a and a))
1369. ((true <-> a) <-> (false or a))
1370. ((true <-> a) <-> (a or false))
1371. ((true <-> a) <-> (a or a))
1372. ((true <-> a) <-> (true -> a))
1373. ((false <-> true) <-> (false and a))
1374. ((false <-> true) <-> (a and false))
1375. ((false <-> a) <-> (a -> false))
1376. ((a <-> true) <-> (not (not a)))
1377. ((a <-> true) <-> (true and a))
1378. ((a <-> true) <-> (a and true))
1379. ((a <-> true) <-> (a and a))
1380. ((a <-> true) <-> (false or a))
1381. ((a <-> true) <-> (a or false))
1382. ((a <-> true) <-> (a or a))
1383. ((a <-> true) <-> (true -> a))
1384. ((a <-> false) <-> (a -> false))
1385. ((a <-> b) <-> (b <-> a))
1386. ((not (true and a)) <-> (not a))
1387. ((not (a and true)) <-> (not a))
1388. ((not (a and a)) <-> (not a))
1389. ((not (false or a)) <-> (not a))
1390. ((not (a or false)) <-> (not a))
1391. ((not (a or a)) <-> (not a))
1392. ((not (true -> a)) <-> (not a))
1393. ((not (true <-> a)) <-> (not a))
1394. ((not (a <-> true)) <-> (not a))
1395. ((a and (not true)) <-> (not true))
1396. ((a and (not a)) <-> (not true))
1397. (((not true) and a) <-> (not true))
1398. (((not a) and a) <-> (not true))
1399. ((a -> (not true)) <-> (not a))
1400. ((a -> (not a)) <-> (not a))
1401. ((a <-> (not true)) <-> (not a))
1402. ((a <-> (not a)) <-> (not true))
1403. (((not true) <-> a) <-> (not a))
1404. (((not a) <-> a) <-> (not true))
1405. ((not (not (not (not a)))) <-> a)
1406. ((not (not (true and a))) <-> a)
1407. ((not (not (a and true))) <-> a)
1408. ((not (not (a and a))) <-> a)
1409. ((not (not (false or a))) <-> a)
1410. ((not (not (a or false))) <-> a)
1411. ((not (not (a or a))) <-> a)
1412. ((not (not (true -> a))) <-> a)
1413. ((not (not (true <-> a))) <-> a)
1414. ((not (not (a <-> true))) <-> a)
1415. ((not (true and (not a))) <-> a)
1416. ((not ((not a) and true)) <-> a)
1417. ((not (false or (not a))) <-> a)
1418. ((not ((not a) or false)) <-> a)
1419. ((not (true -> (not a))) <-> a)
1420. ((not (a -> (not true))) <-> a)
1421. ((not (a -> (not a))) <-> a)
1422. ((not (true <-> (not a))) <-> a)
1423. ((not (a <-> (not true))) <-> a)
1424. ((not ((not true) <-> a)) <-> a)
1425. ((not ((not a) <-> true)) <-> a)
1426. ((true and (not (not a))) <-> a)
1427. ((true and (true and a)) <-> a)
1428. ((true and (a and true)) <-> a)
1429. ((true and (a and a)) <-> a)
1430. ((true and (false or a)) <-> a)
1431. ((true and (a or false)) <-> a)
1432. ((true and (a or a)) <-> a)
1433. ((true and (true -> a)) <-> a)
1434. ((true and (true <-> a)) <-> a)
1435. ((true and (a <-> true)) <-> a)
1436. ((a and (not (not a))) <-> a)
1437. ((a and (true and a)) <-> a)
1438. ((a and (false and b)) <-> false)
1439. ((a and (a and true)) <-> a)
1440. ((a and (a and a)) <-> a)
1441. ((a and (b and false)) <-> false)
1442. ((a and (false or false)) <-> false)
1443. ((a and (a or b)) <-> a)
1444. ((a and (b or a)) <-> a)
1445. ((a and (true -> false)) <-> false)
1446. ((a and (a -> false)) <-> false)
1447. ((a and (b -> a)) <-> a)
1448. ((a and (true <-> false)) <-> false)
1449. ((a and (true <-> a)) <-> a)
1450. ((a and (false <-> true)) <-> false)
1451. ((a and (false <-> a)) <-> false)
1452. ((a and (a <-> true)) <-> a)
1453. ((a and (a <-> false)) <-> false)
1454. (((not (not a)) and true) <-> a)
1455. (((not (not a)) and a) <-> a)
1456. (((true and a) and true) <-> a)
1457. (((true and a) and a) <-> a)
1458. (((false and a) and b) <-> false)
1459. (((a and true) and true) <-> a)
1460. (((a and true) and a) <-> a)
1461. (((a and false) and b) <-> false)
1462. (((a and a) and true) <-> a)
1463. (((a and a) and a) <-> a)
1464. (((false or false) and a) <-> false)
1465. (((false or a) and true) <-> a)
1466. (((a or false) and true) <-> a)
1467. (((a or a) and true) <-> a)
1468. (((a or b) and a) <-> a)
1469. (((a or b) and b) <-> b)
1470. (((true -> false) and a) <-> false)
1471. (((true -> a) and true) <-> a)
1472. (((a -> false) and a) <-> false)
1473. (((a -> b) and b) <-> b)
1474. (((true <-> false) and a) <-> false)
1475. (((true <-> a) and true) <-> a)
1476. (((true <-> a) and a) <-> a)
1477. (((false <-> true) and a) <-> false)
1478. (((false <-> a) and a) <-> false)
1479. (((a <-> true) and true) <-> a)
1480. (((a <-> true) and a) <-> a)
1481. (((a <-> false) and a) <-> false)
1482. ((false or (not (not a))) <-> a)
1483. ((false or (true and a)) <-> a)
1484. ((false or (a and true)) <-> a)
1485. ((false or (a and a)) <-> a)
1486. ((false or (false or a)) <-> a)
1487. ((false or (a or false)) <-> a)
1488. ((false or (a or a)) <-> a)
1489. ((false or (true -> a)) <-> a)
1490. ((false or (true <-> a)) <-> a)
1491. ((false or (a <-> true)) <-> a)
1492. ((a or (not (not a))) <-> a)
1493. ((a or (false and b)) <-> a)
1494. ((a or (a and b)) <-> a)
1495. ((a or (b and false)) <-> a)
1496. ((a or (b and a)) <-> a)
1497. ((a or (false or false)) <-> a)
1498. ((a or (false or a)) <-> a)
1499. ((a or (a or false)) <-> a)
1500. ((a or (a or a)) <-> a)
1501. ((a or (true -> false)) <-> a)
1502. ((a or (true -> a)) <-> a)
1503. ((a or (true <-> false)) <-> a)
1504. ((a or (true <-> a)) <-> a)
1505. ((a or (false <-> true)) <-> a)
1506. ((a or (a <-> true)) <-> a)
1507. (((not true) or (not true)) <-> false)
1508. (((not (not a)) or false) <-> a)
1509. (((not (not a)) or a) <-> a)
1510. (((true and a) or false) <-> a)
1511. (((false and a) or b) <-> b)
1512. (((a and true) or false) <-> a)
1513. (((a and false) or b) <-> b)
1514. (((a and a) or false) <-> a)
1515. (((a and b) or a) <-> a)
1516. (((a and b) or b) <-> b)
1517. (((false or false) or a) <-> a)
1518. (((false or a) or false) <-> a)
1519. (((false or a) or a) <-> a)
1520. (((a or false) or false) <-> a)
1521. (((a or false) or a) <-> a)
1522. (((a or a) or false) <-> a)
1523. (((a or a) or a) <-> a)
1524. (((true -> false) or a) <-> a)
1525. (((true -> a) or false) <-> a)
1526. (((true -> a) or a) <-> a)
1527. (((true <-> false) or a) <-> a)
1528. (((true <-> a) or false) <-> a)
1529. (((true <-> a) or a) <-> a)
1530. (((false <-> true) or a) <-> a)
1531. (((a <-> true) or false) <-> a)
1532. (((a <-> true) or a) <-> a)
1533. ((true -> (not (not a))) <-> a)
1534. ((true -> (true and a)) <-> a)
1535. ((true -> (false and a)) <-> false)
1536. ((true -> (a and true)) <-> a)
1537. ((true -> (a and false)) <-> false)
1538. ((true -> (a and a)) <-> a)
1539. ((true -> (false or a)) <-> a)
1540. ((true -> (a or false)) <-> a)
1541. ((true -> (a or a)) <-> a)
1542. ((true -> (true -> a)) <-> a)
1543. ((true -> (true <-> a)) <-> a)
1544. ((true -> (a <-> true)) <-> a)
1545. (((not a) -> (not true)) <-> a)
1546. (((a -> false) -> false) <-> a)
1547. (((a -> b) -> a) <-> a)
1548. (((false <-> a) -> false) <-> a)
1549. (((false <-> a) -> a) <-> a)
1550. (((a <-> false) -> false) <-> a)
1551. (((a <-> false) -> a) <-> a)
1552. ((true <-> (not (not a))) <-> a)
1553. ((true <-> (true and a)) <-> a)
1554. ((true <-> (false and a)) <-> false)
1555. ((true <-> (a and true)) <-> a)
1556. ((true <-> (a and false)) <-> false)
1557. ((true <-> (a and a)) <-> a)
1558. ((true <-> (false or a)) <-> a)
1559. ((true <-> (a or false)) <-> a)
1560. ((true <-> (a or a)) <-> a)
1561. ((true <-> (true -> a)) <-> a)
1562. ((false <-> (a -> false)) <-> a)
1563. ((a <-> (a -> false)) <-> false)
1564. ((a <-> (a <-> b)) <-> b)
1565. ((a <-> (b <-> a)) <-> b)
1566. (((not true) <-> (not a)) <-> a)
1567. (((not a) <-> (not true)) <-> a)
1568. (((not (not a)) <-> true) <-> a)
1569. (((true and a) <-> true) <-> a)
1570. (((false and a) <-> true) <-> false)
1571. (((a and true) <-> true) <-> a)
1572. (((a and false) <-> true) <-> false)
1573. (((a and a) <-> true) <-> a)
1574. (((false or a) <-> true) <-> a)
1575. (((a or false) <-> true) <-> a)
1576. (((a or a) <-> true) <-> a)
1577. (((true -> a) <-> true) <-> a)
1578. (((a -> false) <-> false) <-> a)
1579. (((a -> false) <-> a) <-> false)
1580. (((a <-> b) <-> a) <-> b)
1581. (((a <-> b) <-> b) <-> a)

One Hundred Propositional Tautologies (4)

; In list of the propositional tautologies from the last article
; in this series, I have found another redundancy. For example,
; both (or true nil) and (or true A) are still in the 100 formulas,
; although (or true nil) is special case of (or true A).

; How it happened? (or true A) is discovered after
; (or true nil). So, tests confirmed that (or true A) is not the instance
; of any tautology, but (or true nil) suddenly became the instance.
; of later developed theorem. And what now?

; (or true nil) becomes some kind of a formula for museum. In time it
; was discovered, it was interesting enough, but now - it cannot
; be effectively used any more in future development. So, what to
; do with that? I'll build special list, and call it museum. OK,
; I could use the word "archive", but this word is somehow overloaded,
; so I'll use museum.
;
; Then, I'll change the program on this way: first,
;
;    (1) it generates all propositional formulas of a given length,
;        making a list PF.
;
;    (2) it filters out tautologies - and makes the list T1
;
;    (3) one by one, it passes through tautologies in T1 and tests
;        whether some of them are instances of other, previously
;        developed tautologies in T1. More than that, it tests
;        whether some of the subformulas of tautologies is an
;        instance of the previously developed tautologies. Only
;        those tautologies, proved not to be an instances are
;        inserted in new list T2.
;
;    (4) Some of the formulas from T2 are "obsolete", because
;        some of the tautologies generated later are more general
;        - more general in a sense - older formula is and instance
;        - of new formula, or some subformula of the older formula
;        is an instance of a newer formula. These formulas are
;        moved to "museum", I'll name it M2.

(load "http://www.instprog.com/Instprog.default-library.lsp")

(set 'PF (apply append (map (lambda(x)(all-pf x '(true nil a b c d e)
                                                '(not)
                                                '(and or -> <->)))
                            (sequence 1 5))))

(println "Generated " (length PF) " formulas.")

(set 'T1 (filter tautology? PF))

(println "Filtered to " (length T1) " tautologies in T1.")

(set 'T2 (list))
(dolist(f1 T1)
   (set 'is-instance nil)
   (dolist(f2 T2 is-instance)
      (let((uf2 (upper-case-formula f2)))
          (dolist (sf1 (difference (branches f1) booleans) is-instance)
            (set 'u (unify sf1 uf2))
            (when (or u (= u '()))
                  (set 'is-instance true)))))
    (unless is-instance
            (push f1 T2 -1)))

(println "Filtered to " (length T2) " tautologies in T2.")

(set 'T2 (reverse T2))
(set 'T3 (list))
(set 'M3 (list))

(dolist(f1 T2)
   (set 'f1counter $idx)
   (set 'is-instance nil)
   (dolist(f2 T2)
     (when (> f1counter $idx)
        (let((uf2 (upper-case-formula f2)))
          (dolist (sf1 (difference (branches f1) booleans) is-instance)
            (set 'u (unify sf1 uf2))
            (when (or u (= u '()))
                  ;(println "--- " f1counter " ---")
                  ;(println= "\nInstance discovered: \n" f1 "\n" sf1 "\n" uf2)
                  (set 'is-instance true))))))
   (if is-instance (push f1 M3)
                   (push f1 T3)))

(println "Filtered to " (length T3) " tautologies in T3 and "
                        (length M3) " tautologies in M3.")

(println "\n\n\n*** T3 ***\n")
(map (lambda(x)(println (+ $idx 1) ". " x)) T3)

(println "\n\n\n*** M3 ***\n")
(map (lambda(x)(println (+ $idx 1) ". " x)) M3)

(exit)

;---------------------------------------------------------------
; OUTPUT

Generated 12971 formulas.
Filtered to 2467 tautologies in T1.
Filtered to 137 tautologies in T2.
Filtered to 84 tautologies in T3 and 53 tautologies in M3.

*** T3 ***

1. true
2. (not nil)
3. (not (not true))
4. (and true true)
5. (or true a)
6. (or a true)
7. (-> nil a)
8. (-> a true)
9. (-> a a)
10. (<-> a a)
11. (not (and nil a))
12. (not (and a nil))
13. (not (or nil nil))
14. (not (-> true nil))
15. (not (<-> true nil))
16. (not (<-> nil true))
17. (or a (not a))
18. (or (not a) a)
19. (-> (not true) a)
20. (<-> nil (not true))
21. (<-> (not true) nil)
22. (not (and a (not true)))
23. (not (and a (not a)))
24. (not (and (not true) a))
25. (not (and (not a) a))
26. (not (or nil (not true)))
27. (not (or (not true) nil))
28. (not (-> true (not true)))
29. (not (<-> a (not a)))
30. (not (<-> (not a) a))
31. (or a (-> a b))
32. (or a (<-> nil a))
33. (or a (<-> a nil))
34. (or (-> a b) a)
35. (or (<-> nil a) a)
36. (or (<-> a nil) a)
37. (-> a (not (not a)))
38. (-> a (and true a))
39. (-> a (and a true))
40. (-> a (and a a))
41. (-> a (or a b))
42. (-> a (or b a))
43. (-> a (-> b a))
44. (-> a (<-> true a))
45. (-> a (<-> a true))
46. (-> (not (not a)) a)
47. (-> (and nil a) b)
48. (-> (and a nil) b)
49. (-> (and a b) a)
50. (-> (and a b) b)
51. (-> (or nil nil) a)
52. (-> (or nil a) a)
53. (-> (or a nil) a)
54. (-> (or a a) a)
55. (-> (-> true nil) a)
56. (-> (-> true a) a)
57. (-> (<-> true nil) a)
58. (-> (<-> true a) a)
59. (-> (<-> nil true) a)
60. (-> (<-> a true) a)
61. (<-> nil (and nil a))
62. (<-> nil (and a nil))
63. (<-> a (not (not a)))
64. (<-> a (and true a))
65. (<-> a (and a true))
66. (<-> a (and a a))
67. (<-> a (or nil a))
68. (<-> a (or a nil))
69. (<-> a (or a a))
70. (<-> a (-> true a))
71. (<-> a (<-> true a))
72. (<-> a (<-> a true))
73. (<-> (not (not a)) a)
74. (<-> (and true a) a)
75. (<-> (and nil a) nil)
76. (<-> (and a true) a)
77. (<-> (and a nil) nil)
78. (<-> (and a a) a)
79. (<-> (or nil a) a)
80. (<-> (or a nil) a)
81. (<-> (or a a) a)
82. (<-> (-> true a) a)
83. (<-> (<-> true a) a)
84. (<-> (<-> a true) a)

*** M3 ***

1. (or true true)
2. (or true nil)
3. (or nil true)
4. (-> true true)
5. (-> nil true)
6. (-> nil nil)
7. (<-> true true)
8. (<-> nil nil)
9. (not (and true nil))
10. (not (and nil true))
11. (not (and nil nil))
12. (-> (not true) nil)
13. (not (and true (not true)))
14. (not (and (not true) true))
15. (not (<-> true (not true)))
16. (not (<-> (not true) true))
17. (or a (-> a nil))
18. (or (-> a nil) a)
19. (-> a (or nil a))
20. (-> a (or a nil))
21. (-> a (or a a))
22. (-> a (-> true a))
23. (-> (and true nil) nil)
24. (-> (and true nil) a)
25. (-> (and true a) a)
26. (-> (and nil true) nil)
27. (-> (and nil true) a)
28. (-> (and nil nil) nil)
29. (-> (and nil nil) a)
30. (-> (and nil a) nil)
31. (-> (and nil a) a)
32. (-> (and a true) a)
33. (-> (and a nil) nil)
34. (-> (and a nil) a)
35. (-> (and a a) a)
36. (-> (or nil nil) nil)
37. (-> (-> true nil) nil)
38. (-> (<-> true nil) nil)
39. (-> (<-> nil true) nil)
40. (<-> nil (and true nil))
41. (<-> nil (and nil true))
42. (<-> nil (and nil nil))
43. (<-> nil (or nil nil))
44. (<-> nil (-> true nil))
45. (<-> nil (<-> true nil))
46. (<-> nil (<-> nil true))
47. (<-> (and true nil) nil)
48. (<-> (and nil true) nil)
49. (<-> (and nil nil) nil)
50. (<-> (or nil nil) nil)
51. (<-> (-> true nil) nil)
52. (<-> (<-> true nil) nil)
53. (<-> (<-> nil true) nil)

---

One Hundred Propositional Tautologies (3)

; 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)
;

---

Why You Do Not Use Lisp? The Results of The Poll.

During early October 2009, I conducted the poll with question "Why you do not use Lisp"? on this blog.

The poll was announced on related Usenet newsgroups comp.lang.lisp, comp.lang.programming, comp.lang.functional, and also on Reddit and Digg sites. I listed 13 reasons, and specified that even people who use Lisp part of the time are called to answer why they do not use it in other part of the time. Lisp here means all Lisp dialects; and it was also specified. In total, 111 people voted, and here are the results, sorted from the most popular to least popular answer. Multiple answers were allowed, and it was total of 264 answers, 2.4 per voter on average.

I use Lisp, at least sometimes.                                                                 49 (44%)
It has not enough support for modern programming practice (libraries, threads and similar.)     42 (37%)
Its syntax repulses me.                                                                         26 (23%)
It is socially inadequate (small, not very alive community.)                                    23 (20%)
It doesn't have any technical advantage I might want.                                           20 (18%)
Its IDE is not good enough.                                                                     18 (16%)
I'd like to use Lisp, but my superiors or colleagues do not want that.                          15 (13%)
It has not enough support for higher level programming (laziness, logic programming...)         15 (13%)
It is socially inadequate (arrogant, unhelping community.)                                      14 (12%)
It is too slow or bloated.                                                                      12 (10%)
It has attractive technical advantages, but these are hard to learn, use and not worth effort.  11  (9%)
It is OK, but only in some commercial version - and I want free or much cheaper one.            10  (9%)
It is so marginal that I never considered it.                                                    9  (8%)

Presented on this way, it is not easy to recognize the message of the poll. All answers are expected, but what their relative importance means? However, I believe we can filter out important information, if we take into account two things: first, voters have much higher than average interest in Lisp and functional or metaprogramming than usually. Those who do not care for Lisp didn't care to vote on this poll as well. About 13% of voters would like to use Lisp, but they cannot because other their colleagues and bosses do not allow it. This is surprisingly low number of people - whatever your favourite language, the chance that your boss will prefer something else is large. If anything can be concluded it is that majority of Lispers somehow managed to group together or work on their own.

Lot of voters (37%) miss some libraries, or support for some modern feature. However, it doesn't say us much: lack of the libraries is universal phenomenon. I believe many people would say they do not use some mainstream language, say, Python because they've found that Ruby, Java or Perl have some specific library supported better. Second, this reason is somehow circular - less libraries means less users etc. Taking it into account, even if Lisp community wrote libraries as no one did, the result wouldn't be much better. It would be much better regarding libraries, but not much regarding programmers. Many of these who complain about lack of libraries probably already use Lisp part of the time.

The second reason is much stronger: 23% of voters do not like Lisp syntax. I incline to think that very few people who do not like Lisp syntax use Lisp on the first place. So, almost the half of the voters who do not use Lisp (56%) - on this poll - do that because of the syntax. If we assume that interest of the voters for Lisp is above average, we can safely say that Lisp syntax is the most important reason for majority of people who do not use Lisp.

One surprise, for me, is popularity of the answers "Lisp doesn't have any technical advantage I may want." (18%) "it has not enough support for higher level programming" (and it includes static typing) (13%) and "It has attractive technical advantages, but these are hard to learn, use and not worth effort" (9%) we have another revealing information - Lisp community didn't succeeded to develop or demonstrate technical advantages of Lisp. Functional languages programmers certainly understand these advantages, but they still think these are not that significant.

Good news is that Lisp got rid of its image as bloated and slow. Only 10% of voters complained about that. For, say, Modula-2, even that would be too much, but for Lisp family, which is certainly not designed to be among the leanest possible languages, the result is quite good.

Social inadequacy, i.e. small, not very alive community - rates surprisingly high (20%). I had no clue that people like to communicate that much. One might think that large community means lot of libraries. It does - but it still doesn't mean that voter will get the library he wants. So, it is, I believe, more of a human instinct for joining large, progressing, vibrant, active community, perhaps related to survival. Well, good information for all Lisp programmers and especially my Newlisp fellows; communication matters. On a related matter, significant number of voters (12%) believe that Lisp users are arrogant and unhelpful community.

Some 16% of voters missed good IDE. Well, two commercial Common Lisps have good IDE, and have free personal versions. PLT Scheme has nice IDE as well. Newlisp has very simple IDE. Personally I use Scite, which is text editor that can cooperate with command line tools easily, and it is good enough for me. About 9% of voters miss something in free versions, and it can be easily that it is again IDE.

Another poll that might interest you:

Opinions on Eval in Lisp, Python and Ruby. The Results of The Poll.

---

Opinions on Eval in Lisp, Python and Ruby - The Results of The Poll.

During September 2009, I made three polls with question "what do you think about eval?" for Lisp, Python and Ruby programmers separately. In total, there were 104 votes, between 30-40 for each language. Here are the results, graph and interpretations:

.                                                  Lisp          %     Python          %       Ruby          %
--------------------------------------------------------------------------------------------------------------
Eval is evil, harmful or at least unnecessary         2        4.9          7       21.9          0        0.0
Eval is useful but overused                          11       26.8          6       18.8          9       29.0
Eval has just the right place                        16       39.0         10       31.3         19       61.3
Eval is useful but neglected                          3        7.3          4       12.5          1        3.2
Eval is a single most important feature               5       12.2          0        0.0          0        0.0
I do not care for eval                                4        9.8          5       15.6          2        6.5
--------------------------------------------------------------------------------------------------------------
Total                                                41      100.0         32      100.0         31      100.0

(Those who voted they do not care about eval are ignored on graph.)

Great majority of Ruby programmers are satisfied with eval, and significant minority believe that eval is useful but overused. That means that Ruby designer should slightly discourage use of eval, or Ruby community should discuss the issue to reach understanding why and how not to use eval, or why use of eval is justified. Rubyists are not extremists - no one has extreme opinion, and it suggests that they have good capacity for cooperation - at least from the point of view of this, single aspect - which is not unimportant, since recently Ruby is frequently discussed in connection with metaprogramming.

The difference between Python programmers is more significant; majority of them think that eval has the right place in Python, and nearly equal number think that it is overused or neglected. However, large number of Python programmers believe that "eval is evil." Such a large group with extreme opinion suggests that Python community might separate in future on the group that wants Python to be more static, probably compiled - and others. Or, one group will prevail, and others will leave.

In Lisp community, it is exactly opposite: almost 15% Lisp programmers think that eval is essential, and about 5% think eval is evil. It is somehow strange that more Lispers than Rubyists are extremely against eval. Both extremes are significant, and it guarantees consistent disagreements and discussions on the topic. That means, community cannot be united - and it is not united, of course. Even in this single issue, fragmentation of Lisp community is justified.

Another possibility is that some Lisp programmers are not attracted by technical merits of the language, but by its allure - result of Lisp's long history, romantic AI past, and compliments given by programmers - celebrities like Yukihiro Matsumoto, Eric S. Raymond, Alan Kay, Paul Graham, Richard Stallman, Gregory Chaitin. However, I believe that those who do not like the language itself, especially its syntax, give up very early.

Comments are welcome.

---

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)

---

One Hundred Propositional Tautologies (1)

; 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.

Debug-wrapping Around Built-in Primitives

; Debug-wrap is one of the most practical functions resulted from
; deliberations on this blog. It is described in this post:
;
; http://kazimirmajorinc.blogspot.com/2008/07/verbose-functions.html
;
; version described in the blog maybe doesn't work any more as it is, 
; because Newlisp changed in the meantime. But essence is the same, and
; updated version is in Instprog.default-library.lsp. 

; Classical examples are Fibonacci's numbers. 

(load "http://www.instprog.com/Instprog.default-library.lsp")

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

(set 'fib (lambda(n)(if (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))))
(debug-wrap fib)

(fib 5)

; 
; Result:
; 
; (fib (in 5)
;      (fib (in 4)
;           (fib (in 3)
;                (fib (in 2)
;                     (out 1))
;                (fib (in 1)
;                     (out 1))
;                (out 2)); t=22
;           (fib (in 2)
;                (out 1))
;           (out 3)); t=43
;      (fib (in 3)
;           (fib (in 2)
;                (out 1))
;           (fib (in 1)
;                (out 1))
;           (out 2)); t=22
;      (out 5)); t=86
;    
; "comments" like t=113 are the time of the evaluation of the function, 
; in microseconds .The result is in form of s-expression, because 
; that is readable format, and also, because it allows one to inspect 
; debugging output in some s-expression aware text editor, that 
; can highlight left and right parenths. I had best experiences
;  with PLT Scheme editor. Debug-wrap can be applied on macros and
; built in primitives as well.

 (debug-wrap +)
 (fib 5)
 
; (fib (in 5)
;      (+ (in (fib (- n 1)) (fib (- n 2)))
;         (fib (in 4)
;              (+ (in (fib (- n 1)) (fib (- n 2)))
;                 (fib (in 3)
;                      (+ (in (fib (- n 1)) (fib (- n 2)))
;                         (fib (in 2)
;                              (out 1))
;                         (fib (in 1)
;                              (out 1))
;                         (out 2)); t=23
;                      (out 2)); t=35
;                 (fib (in 2)
;                      (out 1))
;                 (out 3)); t=57
;              (out 3)); t=71
;         (fib (in 3)
;              (+ (in (fib (- n 1)) (fib (- n 2)))
;                 (fib (in 2)
;                      (out 1))
;                 (fib (in 1)
;                      (out 1))
;                 (out 2)); t=21
;              (out 2)); t=34
;         (out 5)); t=131
;      (out 5)); t=141
;
; OK, it works. But, what will happen if I try something relatively
; naive:
; 
; (debug-wrap when)
; 
; (fib 5) 
;

; 
; Why? The function when is used inside the definition of new, 
; debug version of when. So, when calls another instance of when,
; which calls another instance of when and so forth.
;
; So, what is the solution for this case? We'll replace all occurences
; of symbol when in the body of debug-wrap with symbol [when.original].
; There are few trivial details also. 

(debug-unwrap fib)
(debug-unwrap +)

(set '[when.original] when)
(set 'debug-wrap (expand debug-wrap '((when [when.original]))))

(debug-wrap when)
(debug-wrap fib)

(fib 5)

; it works. Wrapped when is not problem any more. 

; Now, I'll debug-wrap all primitives used in fib: +, - and if. 
; I'll use few functions that semi-automatize that. Main idea is 
; relatively simple, but there are quite a few technical details.
; My suggestion is - don't bother much about details, just get the
; idea. First, I'll clean the tails left from previous debugging
; sessions of fib. 

(debug-unwrap when)
(debug-unwrap fib)

; Function original accepts symbol, say z as argument and returns 
; symbol [z.original]

(set 'original
  (lambda([original.x])
    (sym (append "[" (string [original.x]) 
                     ".original]"))))
                     
; this loop is equivalent to (set '[+.original] +) and same for
; - and if. 

(dolist(i '(+ - if))
  (if (primitive? (eval i))
      (set (original i)
           (eval i))))

; The function originalize replace all simbols like + with [+.original]
; in the body of the fname.

(set 'originalize 
  (lambda(fname symbolist)
    (eval (list (if (protected? (eval fname))
                    'set 
                    'constant)
                'fname 
                (expand (eval fname) 
                        (map (lambda(s)      ;this map will produce
                                (list s      ;((+ [+.original])...)
                                      (original s))) 
                             symbolist))))))                  
                               
                                                       
(originalize 'debug-wrap '(+ - if))
(originalize 'println '(+ - if)) ; I must do that because my library
                                 ; redefines println on the way that
                                 ; contains if, and if I do not use
                                 ; original if, infinite loops is 
                                 ; created.
(originalize 'print '(+ - if))   ; The same as println. 

(debug-wrap fib)
(debug-wrap +)
(debug-wrap -)
(debug-wrap if)
(===)
(fib 5)

(exit)

; RESULT

; (fib (in 5)
;      (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;          (+ (in (fib (- n 1)) (fib (- n 2)))
;             (- (in n 1)
;                (out 4))
;             (fib (in 4)
;                  (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                      (+ (in (fib (- n 1)) (fib (- n 2)))
;                         (- (in n 1)
;                            (out 3))
;                         (fib (in 3)
;                              (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                                  (+ (in (fib (- n 1)) (fib (- n 2)))
;                                     (- (in n 1)
;                                        (out 2))
;                                     (fib (in 2)
;                                          (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                                              (out 1))
;                                          (out 1)); t=10
;                                     (- (in n 2)
;                                        (out 1))
;                                     (fib (in 1)
;                                          (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                                              (out 1))
;                                          (out 1)); t=14
;                                     (out 2)); t=64
;                                  (out 2)); t=78
;                              (out 2)); t=89
;                         (- (in n 2)
;                            (out 2))
;                         (fib (in 2)
;                              (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                                  (out 1))
;                              (out 1)); t=11
;                         (out 3)); t=143
;                      (out 3)); t=153
;                  (out 3)); t=164
;             (- (in n 2)
;                (out 3))
;             (fib (in 3)
;                  (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                      (+ (in (fib (- n 1)) (fib (- n 2)))
;                         (- (in n 1)
;                            (out 2))
;                         (fib (in 2)
;                              (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                                  (out 1)); t=1
;                              (out 1)); t=13
;                         (- (in n 2)
;                            (out 1))
;                         (fib (in 1)
;                              (if (in (< n 3) 1 (+ (fib (- n 1)) (fib (- n 2))))
;                                  (out 1))
;                              (out 1)); t=13
;                         (out 2)); t=75
;                      (out 2)); t=88
;                  (out 2)); t=101
;             (out 5)); t=302
;          (out 5)); t=311
;      (out 5)); t=325
;

; In next few weeks, I'll integrate all that in the library, so use of the
; debug-wrap will be simpler even when built-in primitives are 
; debug-wrapped.

Kazimir Majorinc's Programming Notes.

Relatively Short Propositional Formulas and Symbols Instead of Pointers and Tables.

Tortelvis.

One Hundred Propositional Tautologies (5)

One Hundred Propositional Tautologies (4)

One Hundred Propositional Tautologies (3)

Why You Do Not Use Lisp? The Results of The Poll.

Opinions on Eval in Lisp, Python and Ruby - The Results of The Poll.

One Hundred Propositional Tautologies (2)

One Hundred Propositional Tautologies (1)

Debug-wrapping Around Built-in Primitives

Do you like the colour combination used in this blog?

The Most Popular Posts.

Archive

Search

My Web Site

Alexa Site Info

Newlisp Related Sites.

Newlisp Related Blogs

Followers

Kazimir Majorinc's Programming Notes.

Do you like the colour combination used in this blog?

The Most Popular Posts.

Subscribe

Archive

Search

My Web Site

Alexa Site Info

Newlisp Related Sites.

Newlisp Related Blogs

Followers