```JOY  -  compiled at 14:54:45 on Feb  1 2002 (BDW)
Copyright 2001 by Manfred von Thun

testing the propositional logic library in file  plglib.joy

(* There are many notations. Begin using minimally bracketed infix:	*)

DEFINE   m-show == Min2Tre taut-show-all.

[ raining or not raining ]				m-show.
tautology

[ raining or not windy ]				m-show.
not tautology, countermodel(s):
1 	T: [windy]   F: [raining]

[ [p and q] imp [p or q] ]				m-show.
tautology

[ [p or q] imp [p and q] ]				m-show.
not tautology, countermodel(s):
1 	T: [p]   F: [q]
2 	T: [q]   F: [p]

(* Really using minimal bracketing on the last two examples:		*)

[ p and q  imp  p or q ]				m-show.
tautology

[ p or q  imp  p and q ]				m-show.
not tautology, countermodel(s):
1 	T: [p]   F: [q]
2 	T: [q]   F: [p]

(* Longer examples show the benefit of minimal bracketing:		*)

[ p and q and r imp  p or r or q ]			m-show.
tautology

[ p and q and r iff  p or r or q ]			m-show.
not tautology, countermodel(s):
1 	T: [p]   F: [q]
2 	T: [p]   F: [r]
3 	T: [r]   F: [p]
4 	T: [r]   F: [q]
5 	T: [q]   F: [p]
6 	T: [q]   F: [r]

(* Using a more compact single symbol notation:				*)

[ p & q & r & s  >  p v r v q v s ]			m-show.
tautology

[ p & q & r & s  =  p v r v q v s ]			m-show.
not tautology, countermodel(s):
1 	T: [p]   F: [q]
2 	T: [p]   F: [r]
3 	T: [p]   F: [s]
4 	T: [r]   F: [p]
5 	T: [r]   F: [q]
6 	T: [r]   F: [s]
7 	T: [q]   F: [p]
8 	T: [q]   F: [r]
9 	T: [q]   F: [s]
10 	T: [s]   F: [p]
11 	T: [s]   F: [q]
12 	T: [s]   F: [r]

[ - p & - q   >  - [p v q] ]				m-show.
tautology

[ - p v - p   >   - [p v q] ]				m-show.
not tautology, countermodel(s):
1 	T: [q]   F: [p]
2 	T: [q]   F: [p]

[ p > q > r > p & q & r ]				m-show.
tautology

[ p > q > r > p & q & s ]				m-show.
not tautology, countermodel(s):
1 	T: [r q p]   F: [s]

[ [[p > q]  >  p]   >   p  ]				m-show.
tautology

[ [[p > q]  >  q]   >   p  ]				m-show.
not tautology, countermodel(s):
1 	T: [q]   F: [p]

[ [ p & q v p & r ]  =  p & [q v r] ]			m-show.
tautology

[ [ p & q v p & r ]  =  q & [p v r] ]			m-show.
not tautology, countermodel(s):
1 	T: [r p]   F: [q]
2 	T: [r q]   F: [p]

[ [p v q] & [p > r] & [q > s]   >   [r v s] ]		m-show.
tautology

[ [p v q] & [p > r] & [q > s]   >   [r & s] ]		m-show.
not tautology, countermodel(s):
1 	T: [r p]   F: [s q]
2 	T: [s q]   F: [r p]

(* The original Polish notation, used by Polish logicians in the 1920's	*)
(* N = not, K = and, A = or, C = imp, E = iff :				*)

DEFINE   p-show == Pol2Tre taut-show-all.

[  A  p  N p  ]						p-show.
tautology

[  A  p  N q  ]						p-show.
not tautology, countermodel(s):
1 	T: [q]   F: [p]

[  C   C p q   C N q N p  ]				p-show.
tautology

[  C   C p q   C N p N q  ]				p-show.
not tautology, countermodel(s):
1 	T: [q]   F: [p]
2 	T: [q]   F: [p]

[  C  K  K  A p q  C p r  C q s   A r s  ]		p-show.
tautology

[  C  K  K  A p q  C p r  C q s   K r s  ]		p-show.
not tautology, countermodel(s):
1 	T: [r p]   F: [s q]
2 	T: [s q]   F: [r p]

(* But we can also use the other symbols for Polish notation:		*)

[ imp  and  imp p q  imp q r   imp p r ]		p-show.
tautology

[ imp  and  imp p q  imp p r   imp q r ]		p-show.
not tautology, countermodel(s):
1 	T: [q]   F: [r p]
2 	T: [q]   F: [r p]

[ >  v p & q r   & v p q v p r ]			p-show.
tautology

[ >  v p & q r   v & p q & p r ]			p-show.
not tautology, countermodel(s):
1 	T: [p]   F: [r q]
2 	T: [r q]   F: [p]

(* Using reverse Polish (postfix, Joy) notation:			*)

DEFINE   r-show == Rev2Tre taut-show-all.

[ p not q not and r imp   q p or  not   and  r  imp ]	r-show.
tautology

[ p not q not and r imp   q p and not   and  r  imp ]	r-show.
not tautology, countermodel(s):
1 	T: [p]   F: [r q]
2 	T: [q]   F: [r p]

(* The remaining tests only use minimally bracketed infix for input.	*)
(* There are four additional versions of the possible output:		*)

(* 1. Instead of showing all countermodels, show only one:		*)

DEFINE   m-show1 == Min2Tre taut-show-first.

[ p & q & r  >  p v q v r ]				m-show.
tautology

[ p v q v r  >  p & q & r ]				m-show.
not tautology, countermodel(s):
1 	T: [p]   F: [q]
2 	T: [p]   F: [r]
3 	T: [q]   F: [p]
4 	T: [q]   F: [r]
5 	T: [r]   F: [p]
6 	T: [r]   F: [q]

[ p v q v r  >  p & q & r ]				m-show1.
not tautology, first countermodel:
T: [p]   F: [q]

(* 2. Do not show, but collect into  list (for further processing ?):	*)

DEFINE   m-collect  == Min2Tre taut-collect-all;
m-collect1 == Min2Tre taut-collect-first.

[ [p > q] & [q > s]   >   [p > s] ]			m-collect.
[]

[ [p > q] & [q > s]   >   [s > p] ]			m-collect.
[[[s q] [p]] [[s] [p]] [[s] [q p]]]

[ [p > q] & [q > s]   >   [s > p] ]			m-collect1.
[[[s] [q p]]]

(* 3. Do not show or collect, just return number of countermodels:	*)

DEFINE   m-count == Min2Tre taut-count.

[ [p > q] & [r > s]   >  [[p & r] > [q v s]] ]		m-count.
0

[ [p > q] & [r > s]   >  [[p v r] > [q & s]] ]		m-count.
2

[ [p > q] & [r > s]   >  [[p v r] > [q & s]] ]		m-show.
not tautology, countermodel(s):
1 	T: [r s]   F: [q p]
2 	T: [p q]   F: [s r]

(* 4. Disregard countermodels, just determine whether tautology:	*)

DEFINE   m-test == Min2Tre taut-test.

[ [p & q & r]  >  [p = q = r] ]				m-test.
true

[ [p = q = r]  >  [p & q & r] ]				m-test.
false

[ [p = q = r]  >  [p v q v r] ]				m-test.
true

[ [p v q v r]  >  [p = q = r] ]				m-test.
false

(* Finally, for big formulas it can be useful to give a definition:	*)
(* Also, it can help to set them out over several lines:		*)

DEFINE big-formula ==
[  [ CEO-sells-shares
imp    CEO-resigns  or  CEO-is-sacked ]			and
[ CEO-resigns
imp    i-trade-exposed  and  shares-drop ]		and
imp    sales-drop ]					and
[ sales-drop
imp    CEO-is-sacked  and  shares-drop ]
imp
[ CEO-sells-shares
imp    shares-drop ]  ].

big-formula  m-test.
false

big-formula  m-show.
not tautology, countermodel(s):