JOY  -  compiled at 14:54:45 on Feb  1 2002 (BDW)
Copyright 2001 by Manfred von Thun
usrlib  is loaded
inilib  is loaded
agglib  is loaded

testing the propositional logic library in file  plglib.joy

agglib  is already loaded
numlib  is loaded
agglib  is already loaded
seqlib  is loaded
symlib  is loaded
plglib  is loaded
 
(* 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    insider-trading  and  traders-conspire ]		and 
     [ i-trade-exposed 
	imp    CEO-resigns  or  CEO-is-sacked ]			and 
     [ CEO-resigns 
	imp    i-trade-exposed  and  shares-drop ]		and 
     [ traders-conspire  and  CEO-is-sacked 
	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):
  1 	T: [CEO-sells-shares traders-conspire insider-trading]   F: [shares-drop sales-drop CEO-is-sacked CEO-resigns i-trade-exposed] 
 
(* So, it ain't half as bad as long as you let them get away with it...	*) 
 
(* end  plgtst.joy *)