; GROUP: PROPOSITIONAL VARIABLES AND FORMULAS ; ; Description: Few elementary functions related to propositional ; formulas, implemented on the simplest way. ; Some of the functions can redefine values of ; the variables in the propositional formulas. ; ; They use some other library functions I wrote, ; so this code cannot be just cutted and pasted ; in editor, but I'll publish it in library soon ; (or I already did it.) ; ; Names: propositional-variables, PV ; ; tautology ; falsifiable ; satisfiable ; contradiction ; ; satisfaction ; falsification ; ; Type: functions ; ; Examples: (propositional-variables '(-> nil (-> nil nil))) ; ===> '() ; ; (propositional-variables '(-> A (or B (and D true) nil))) ; ===> '(A B D) ; ; (tautology? '(-> A B)) ==> nil ; ; (tautology? (-> nil (-> nil nil))) ==> true ; ; (falsifiable '(-> A B)) ==> true ; ; (falsifiable (-> nil (-> nil nil))) ==> nil ; ; (falsification '(-> A B)) ==> ((A true) (B nil)) ; ; (satisfaction '(-> A (not A))) ==> '((A nil))) ; (SU 'propositional-variables ; SU is my version of set, it warns ; if variable is already defined (lambda(f)(difference (unique (leafs f)) ; (leafs '(-> (-> x y) z)) ==> (x y z) booleans))) ; booleans = '(true nil) (SU 'PV propositional-variables) (P1S 'propositional-variables '(f)) ; P1S is my protection ; function roughly equivalent ; to built in contexts. ; I use it instead of contexts ; primarily because I can ; experiment. (P1S 'PV '(f)) (test "propositional-variables 1" (= (propositional-variables '(-> nil (-> nil nil))) '())) ; -> is implication, the propositional logical ; connective like or and not, defined ; earlier in library. (test "propositional-variables 2" (= (propositional-variables '(-> A (or B (and D true) nil))) '(A B D))) (SU 'tautology? (lambda(formula) (let ((tautology true)) (letex ((L (propositional-variables formula))) (dolist-multi(L booleans (not tautology)) (setand 'tautology (eval formula)))) ; (setand 'x y) = (set 'x (and x y)) tautology))) (test "tautology" (not (tautology? '(-> A B)))) (test "tautology2" (tautology? (-> nil (-> nil nil)))) (SU 'falsifiable? (not^ tautology?)) ; not^ is a higher order not; ; it can be applied on functions ; ((not^ f) x) = (not (f x)) ; for every x (test "falsifiable? 1" (not (falsifiable? true))) (test "falsifiable? 2" (falsifiable? '(-> A B))) (P1S 'tautology? '(formula tautology L)) (P1S 'falsifiable? '(formula tautology L)) (SU 'falsification (lambda(formula) (let ((tautology true) (result nil)) (letex ((L (propositional-variables formula))) (dolist-multi(L booleans (not tautology)) (setand 'tautology (eval formula)) (unless tautology (set 'result (map (lambda(x)(list x (eval x))) 'L))))) result))) (test "falsification" (= (falsification '(-> A B)) '((A true) (B nil)))) (P1S 'falsification '(formula tautology result L)) (SU 'satisfiable? (lambda(f)(falsifiable? (list 'not f)))) (SU 'satisfaction (lambda(f)(falsification (list 'not f)))) (SU 'contradiction? (not^ satisfiable?)) (test "satisfaction" (= (satisfaction '(-> A (not A))) '((A nil)))) (P1S 'satisfiable? '(f)) (P1S 'satisfaction '(f)) (P1S 'contradiction? '(f))
Related posts: Random Propositional Formulas of a Given Lenght, 2009. |