### 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
;
;               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))))