examples/logics.rkt
```#lang racket
;; =====================================================================
;; An example of using rewriting in symbolic computations.
;; Expansion of logical expressions to CNF an DNF.
;; =====================================================================
(require (planet "main.rkt" ("samsergey" "rewrite.plt" 1 0))
rackunit)

;; declare this symbols to denote formal functions
(define-formal && || !)

;; =====================================================================
;; parsing infix notation
;; =====================================================================
(define infix->prefix
(replace-all-repeated
`(,a __1  <=> ,b __1) --> (&& `(,a => ,b) `(,b => ,a))
`(,a __1  =>  ,b __1) --> (|| b (! a))
`(,a __1  ||  ,b __1) --> (|| a b)
`(,a __1  &&  ,b __1) --> (&& a b)
`(,a) -->  a))

;; =====================================================================
;; simplification of expressions
;; =====================================================================
(define ordered?
; ordering of terms
(replace
(? symbol? x) (? symbol? y) --> (string<=? (symbol->string x) (symbol->string y))
(? symbol?) (? pair?)  --> #t
(cons a x) (cons a y) --> (ordered? x y)
(cons x _) (cons y _) --> (ordered? x y)
_ _ --> #f ))

(define simplify
(replace-all-repeated
; exclusion of parenthesis
`(,a) --> a

; degenetare cases
(|| a)  -->  a
(||)    --> 'F
(&& a)  -->  a
(&&)    --> 'T

; negation propertyes
(! (! a))  -->  a
(! 'F)     --> 'T
(! 'T)     --> 'F

; conjunction properties
(&& _ ___ 'F _ ___)            --> 'F
(&& x ___ 'T y ___)            --> `(&& ,@x ,@y)
(&& x ___ A y ___ A z ___)     --> `(&& ,@x ,A ,@y ,@z)
(&& _ ___ A _ ___ (! A) _ ___) --> 'F

; disjunction properties
(|| _ ___ 'T _ ___)            --> 'T
(|| x ___ 'F y ___)             --> `(|| ,@x ,@y)
(|| x ___ A y ___ A z ___)     --> `(|| ,@x ,A ,@y ,@z)
(|| _ ___ A _ ___ (! A) _ ___) --> 'T

; associativity
(&& a ___ (&& b __1) c ___) --> `(&& ,@a ,@b ,@c)
(|| a ___ (|| b __1) c ___) --> `(|| ,@a ,@b ,@c)

; grouping of conjuncts
(|| x ___ A y ___ (&& _ ___ A _ ___) z ___)     --> `(|| ,@x ,A ,@y ,@z)
(|| x ___ A y ___ (&& p ___ (! A) q ___) z ___) --> `(|| ,@x ,A ,@y (&& ,@p ,@q) ,@z)
(|| x ___ (! A) y ___ (&& p ___ A q ___) z ___) --> `(|| ,@x (! ,A) ,@y (&& ,@p ,@q) ,@z)

; grouping of disjuncts
(&& x ___ A y ___ (|| _ ___ A _ ___) z ___) --> `(&& ,@x ,A ,@y ,@z)
(&& x ___ A y ___ (|| p ___ (! A) q ___) z ___) --> `(&& ,@x ,A ,@y (|| ,@p ,@q) ,@z)
(&& x ___ (! A) y ___ (|| p ___ A q ___) z ___) --> `(&& ,@x (! ,A) ,@y (|| ,@p ,@q) ,@z)

; sorting terms to strength normalizing property of the rewriting system
(cons op x) -->  (cons op (sort (map simplify x) ordered?))))

;; =====================================================================
;; Expansion to disjunctive normal form
;; =====================================================================
(define DNF
(compose simplify
(replace-all-repeated
; de Morgan's laws
(! (|| a b __1))  --> (&& (! a) (! `(|| ,@b)))
(! (&& a b __1))  --> (|| (! a) (! `(&& ,@b)))

; distributivity
(&& a ___ (|| b bb __1) c ___) --> `(|| (&& ,@a ,b ,@c)
(&& ,@a (|| ,@bb) ,@c))

; repeating of the expansion
(cons op x) -->  (cons op (map DNF x)))))

;; =====================================================================
;; Expansion to conjunctive normal form
;; =====================================================================
(define CNF
(compose simplify
(replace-all-repeated
; de Morgan's laws
(! (|| a b __1))  --> (&& (! a) (! `(|| ,@b)))
(! (&& a b __1))  --> (|| (! a) (! `(&& ,@b)))

; distributivity
(|| a ___ (&& b bb __1) c ___) --> `(&& (|| ,@a ,b ,@c)
(|| ,@a (&& ,@bb) ,@c))

; repeating of the expansion
(cons op x) --> (cons op (map CNF x)))))

(define expand (compose DNF CNF infix->prefix))

;; =====================================================================
;; Examples
;; =====================================================================

(check-equal? (expand '((A || B) && C))           '(|| (&& A C) (&& B C)))
(check-equal? (expand '((B || A) && (A || ! B)))  'A)
(check-equal? (expand '((A || B) && B))           'B)

(check-equal? (expand '((A => B) && A))      '(&& A B))
(check-equal? (expand '(A => ! A))           '(! A))

;; Tautology proving
(check-eq?
(expand '(A || ! A))
'T)

(check-eq?
(expand '((A => B) <=> (! B => ! A)))
'T)

(check-eq?
(expand '((! A => B) && (! A => ! B) => A))
'T)

(check-eq?
(expand '((human => mortal) && (Socrates => human) => (Socrates => mortal)))
'T)

(check-eq?
(expand '((A || B) && (A => C) && (B => C) => C))
'T)

(check-equal?
(expand '(((P => Q) => P) => P))
'T)

(check-equal?
(expand '((p || ! r) && s => (r && s => (p && q) || p)))
'T)

(check-equal?
(expand '((A && B => C) <=> (A => (B => C))||(B => (A => C))))
'T)

(check-equal? (expand '((A && B) => (A || B))) 'T)

(check-equal?
(expand '(((A <=> B) <=> C) <=> (A <=> (B <=> C))))
'T)

(check-equal?
(expand '(((A || B => A || C) <=> (A || (B => C)))))
'T)
```