(*****************************************************************************
                  CSC 590 Predicate Calculus Exercise #3 Solutions

    Written by;  Dan Stearns, Fall 1994

    Notes
    1.  read section 7.5 of the RSL reference manual on quantifiers
    2.  An axiom is an invariant or universal truth 
    3.  The first 3 are written in two forms using the trading theorms of
        Chapter 9

 *****************************************************************************)

object Human;
value jj:Human =  "Judge Jones";

(* Each of these operations returns true if the Human meets the condition *)
op Cx(Human) -> boolean;    (*  Congressperson *)
op Jx(Human) -> boolean;    (*  Judge *)
op Lx(Human) -> boolean;    (*  Lawyer *)
op Ox(Human) -> boolean;    (*  Old *)
op Px(Human) -> boolean;    (*  Politician *)
op Sx(Human) -> boolean;    (*  Shyster *)
op Wx(Human) -> boolean;    (*  Woman *)
op Vx(Human) -> boolean;    (*  Vigorous *)
op admire(a:Human,b:Human) -> boolean;
(* returns true if a admires b *)


(*  EXERCISES *)

(* a - All Lawyers are judges *)
axiom A = forall (h:Human | Lx(h)) Jx(h);
 (*  <using trading theorm 9.2> *)
axiom A2 = forall (h:Human | Lx(h) implies Jx(h)) true;

(* b - Some lawyers are shysters *)
axiom B = exists (h:Human | Lx(h)) Sx(h);
  (*  <using trading theorm 9.19> *)
axiom B2 = exists (h:Human | Lx(h) and Sx(h)) true;

(* c - No judge is a shyster *)
axiom C = forall (h:Human | Jx(h)) not(Sx(h));
  (* <using trading theorm 9.2> *)
axiom C2 = forall (h:Human | Jx(h) implies not(Sx(h))) true;

(* d - Some judges are old but vigorous *)
axiom D = exists (h:Human | Jx(h)) Ox(h) and Vx(h);

(* e - Judge Jones is neither old nor vigorous *)
axiom E = not(Ox(jj)) and not(Vx(jj));

(* f - Not all lawyers are judges *)
axiom F = not (forall (h:Human | Lx(h)) Jx(h));

(* g - Some lawyers who are politicians are congressmen *)
axiom g =exists (h:Human | Lx(h) and Px(h)) Cx(h);

(* h - No congressman is not vigorous *)
axiom H = forall (h:Human | Cx(h)) not(Vx(h));

(* i - All congressmen who are old are lawyers *)
axiom I = forall (c:Human | Cx(c) and Ox(c)) Lx(c);

(* j - Some women are both lawyers and congresswomen *)
axiom J = exists (w:Human | Wx(w)) Cx(w);

(* k - No woman is both a politican and housewife *)
axiom K = forall (h:Human | Wx(h)) not(Px(h) and Hx(h));

(* l - There are some women lawyers who are housewives *)
axiom L = exists (h:Human | Wx(h) and Lx(h)) Hx(h);

(* m - All women who are lawyers admire some judge *)
axiom M = forall (h:Human | Wx(h) and Lx(h)) exists (j:Human | Jx(j)) admire(h,j); 

(* n - Some lawyers admire only judges *)
axiom N = exists (h:Human | Lx(h)) forall (j:Human | admire(h,j)) Jx(j);

(* o - Some lawyers admire women *)
axiom O = exists (h:Human | Lx(h)) exists (w:Human | Wx(w)) admire(h,w);

(* p - Some shysters admire no lawyer *)
axiom P = exists (s:Human | Sx(s)) forall (l:Human | Lx(l)) not(admire(s,l));

(* q - Judge Jones doesn't admire any shyster *)
axiom Q = forall (s:Human | admire(jj,Sx(s)))  false;
   (*  alternatively *)
axiom Q2 = forall (h:Human | admire(jj,h)) not(Sx(h));

(* r - There are both lawyers and shysters who admire Judge Jones *)
axiom R = exists (l:Human | Lx(l)) admire(l,jj) and 
      exists (s:Human | Sx(s)) admire(s,jj);

(* s - Only judges admire judges *)
axiom S = forall (j:Human | Jx(j)) forall (h:Human | admire(h,j)) Jx(h); 

(* t - All judges admire only judges *)
axiom T = forall (j1:Human | Jx(j1)) forall (j2:Human | admire(j1,j2)) Jx(j2);