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. 




No comments:

Post a Comment