Propositional Variables and Formulas.

; 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.