### Lists of Propositional Formulas

 ; We continue discussing propositional formulas. After few ; functions for generation of random propositional formulas are defined, ; in this post we publish function that generate the list of all ; propositional formulas defined with ; ;  * length of the list ;  * list of leafs (logical constants and variables) ;  * list of unary logical connectives ;  * list of binary logical connectives. ; ; For example, (all-pf 4 '(a b c) '(not) '(and or ->)) is: ; ; ((not (not (not a))) (not (not (not b))) (not (not (not c))) ;  (not (and a a)) (not (and a b)) (not (and a c)) (not (and b a)) ;  (not (and b b)) (not (and b c)) (not (and c a)) (not (and c b)) ;  (not (and c c)) (not (or a a)) (not (or a b)) (not (or a c)) ;  (not (or b a)) (not (or b b)) (not (or b c)) (not (or c a)) ;  (not (or c b)) (not (or c c)) (not (-> a a)) (not (-> a b)) ;  (not (-> a c)) (not (-> b a)) (not (-> b b)) (not (-> b c)) ;  (not (-> c a)) (not (-> c b)) (not (-> c c)) (and a (not a)) ;  (and a (not b)) (and a (not c)) (and b (not a)) (and b (not b)) ;  (and b (not c)) (and c (not a)) (and c (not b)) (and c (not c)) ;  (and (not a) a) (and (not a) b) (and (not a) c) (and (not b) a) ;  (and (not b) b) (and (not b) c) (and (not c) a) (and (not c) b) ;  (and (not c) c) (or a (not a)) (or a (not b)) (or a (not c)) ;  (or b (not a)) (or b (not b)) (or b (not c)) (or c (not a)) ;  (or c (not b)) (or c (not c)) (or (not a) a) (or (not a) b) ;  (or (not a) c) (or (not b) a) (or (not b) b) (or (not b) c) ;  (or (not c) a) (or (not c) b) (or (not c) c) (-> a (not a)) ;  (-> a (not b)) (-> a (not c)) (-> b (not a)) (-> b (not b)) ;  (-> b (not c)) (-> c (not a)) (-> c (not b)) (-> c (not c)) ;  (-> (not a) a) (-> (not a) b) (-> (not a) c) (-> (not b) a) ;  (-> (not b) b) (-> (not b) c) (-> (not c) a) (-> (not c) b) ;  (-> (not c) c)) ; ; All should be here.   (load "http://www.instprog.com/Instprog.default-library.lsp") ; The function *list is "product" of two lists, Cartesian product. ; with few experiments, I discovered that "imperative" version is ; about three times faster than "functional." (set '*list (lambda(l1 l2)               (let ((result '()))                    (dolist(i l1)                      (dolist(j l2)                        (push (list i j) result -1)))                    result))) (println (*list '(1 2 3) '(4 5 6))) ; => ((1 4) (1 5) (1 6) (2 4) (2 5) (2 6) (3 4) (3 5) (3 6)) ; another helper function (set 'appendall (lambda(a b)                   (apply append (map a b))))                  (println (appendall (lambda(x)(list x (sqrt x x)))                     '(1 2 3 4 5))) ;(1 1 2 1.414213562 3 1.732050808 4 2 5 2.236067977) ; Finally, the function. (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)                      '())))))   ;Using this function, it is easy to count number of tautologies: (set 'formulas (all-pf 7 '(true nil a b c) '(not) '(and or ->))) (println '(all-pf 7 '(true nil a b c) '(not) '(and or ->)) " contains "    (length formulas) " formulas and " (length (filter true? (map tautology? formulas)))    " of these are tautologies.") ; (all-pf 7 '(true nil a b c) '(not) '(and or ->)) contains 119255 ; formulas and 39150 of these are tautologies. ; ; Again, we can be surprised how many formulas are actually ; tautologies.