; 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