; 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)
---
No comments:
Post a Comment