Demonstration of SNePSLOG Version of The Jobs Puzzle
demonstrating non-standard connectives and quantifiers

   Welcome to SNePSLOG (A logic interface to SNePS)

Copyright (C) 1984--2007 by Research Foundation of
State University of New York. SNePS comes with ABSOLUTELY NO WARRANTY!
Type `copyright' for detailed copyright information.
Type `demo' for a list of example applications.

: demo
Available demonstrations:
  1:  Socrates - Is he mortal?
  2:  UVBR - Demonstrating the Unique Variable Binding Rule
  3:  The Jobs Puzzle - A solution with the Numerical Quantifier
  4:  Pegasus - Why winged horses lead to contradictions
  5:  Schubert's Steamroller
  6:  Rule Introduction - Various examples
  7:  Examples of various SNeRE constructs.
  8:  Enter a demo filename
Your choice (q to quit): 3

File /projects/snwiz/Install/Sneps-2.7.0/demo/snepslog/jobspuzzle.snlog is now the source of input.

  The demo will pause between commands, at that time press
  RETURN to continue, or ? to see a list of available commands


 CPU time : 0.00 

: ;;; -*- Mode:Common-Lisp; Package:SNEPS; Base:10 -*-
;;;
;;; THE JOBS PUZZLE
;;; A SNePS Exercise demonstrating non-standard connectives and quantifiers
;;; by Stuart C. Shapiro
;;; based on
;;; The Jobs Puzzle in Full, Chapter 3.2
;;; of Automated Reasoning: Introduction and Applications
;;; by Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle
;;; Prentice-Hall, Englewood Cliffs, NJ, 1984, pp. 55-58.
;;;
;;; Most inputs below are preceded by a line labelled "jp:",
;;;      which comes directly from the statement of the jobs puzzle,
;;;      p. 55 of Wos et al.
;;; and some lines labelled "inf", which are permissable immediate
;;; inferences from the puzzle statement according to page 56 or
;;; Chapter 3.2.1, "The Solution by Person or Persons Unknown"
;;; of Wos et al.
;;; and some lines labelled "scs:", which are my comments.
;;;
clearkb
--- pause ---c
Knowledge Base Cleared


 CPU time : 0.01 

: ;;;
;;; jp: There are four people: Roberta, Thelma, Steve, and Pete.
Person({"Roberta", "Thelma", "Steve", "Pete"}).

  wff1!:  Person({Pete,Steve,Thelma,Roberta})    

 CPU time : 0.00 

: ;;;
;;; jp: The jobs are: chef, guard, nurse, telephone operator, police
;;;     officer (gender not implied), teacher, actor, and boxer.
Job({"chef", "guard", "nurse", "telephone operator",
	   "police officer", "teacher", "actor", "boxer"}).

  wff2!:  Job({boxer,actor,teacher,police officer,telephone operator,nurse,guard,chef})    

 CPU time : 0.00 

: ;;;
;;; jp: Among [the people], they hold eight different jobs.
;;; jp: Each holds exactly two jobs.
all(p)(Person(p) => nexists(2,2,8)(j)({Job(j)}: {Is(p,j)})).

  wff3!:  all(p)(Person(p) => (nexists(2,2,8)(j)[{Job(j)}:{Is(p,j)}]))    

 CPU time : 0.00 

: ;;;
;;; inf: "No job is held by more than one person."
all(j)(Job(j) => nexists(1,1,4)(p)({Person(p)}: {Is(p,j)})).

  wff4!:  all(j)(Job(j) => (nexists(1,1,4)(p)[{Person(p)}:{Is(p,j)}]))    

 CPU time : 0.00 

: ;;;
;;; inf: "if the four names did not clearly imply the sex of the people,
;;; [the puzzle] would be impossible to solve."
Female({"Roberta", "Thelma"}).

  wff5!:  Female({Thelma,Roberta})    

 CPU time : 0.00 

: Male({"Steve", "Pete"}).

  wff6!:  Male({Pete,Steve})    

 CPU time : 0.00 

: ;;;
;;; jp: The job of nurse is held by a male.
;;; inf: "everyday language distinguishes [actors and actresses] based
;;;      on sex."
;;; jp: The husband of the chef is the telephone operator.
;;; inf: "the implicit fact that husbands are male"
;;; scs: So neither the nurse, the actor, nor the telephone operator is
;;;      a woman.
all(w)(Female(w)
       => andor(0,0)
               {Is(w, "nurse"), Is(w, "actor"),Is(w, "telephone operator")}).

  wff7!:  all(w)(Female(w) => (andor(0,0){Is(w,telephone operator),Is(w,actor),Is(w,nurse)}))    

 CPU time : 0.00 

: ;;;
;;; inf: since the chef has a husband, she must be female.
all(m)(Male(m) => ~Is(m, "chef")).

  wff8!:  all(m)(Male(m) => (~Is(m,chef)))    

 CPU time : 0.00 

: ;;;
;;; jp: Roberta is not a boxer.
~Is("Roberta", "boxer").

  wff10!:  ~Is(Roberta,boxer)    

 CPU time : 0.00 

: ;;;
;;; jp: Pete has no education past the ninth grade.
;;; inf: "the jobs of nurse, police officer, and teacher each require
;;;      more than a ninth-grade education."
;;; scs: So Pete is neither the nurse, the police officer, nor the teacher.
andor(0,0) {Is("Pete", "nurse"),
            Is("Pete", "police officer"), Is("Pete", "teacher")}.

  wff14!:  andor(0,0){Is(Pete,teacher),Is(Pete,police officer),Is(Pete,nurse)}    

 CPU time : 0.00 

: ;;;
;;; jp: Roberta, the chef, and the police officer went golfing together.
;;; inf: "Thus, we know that Roberta is neither the chef nor the police
;;;      officer."
andor(0,0){Is("Roberta", "chef"), Is("Roberta", "police officer")}.

  wff17!:  andor(0,0){Is(Roberta,police officer),Is(Roberta,chef)}    

 CPU time : 0.00 

: ;;;
;;; inf: "Since they went golfing together, the chef and the police
;;;      officer are not the same person."
all(p)(Person(p) => andor(0,1){Is(p, "chef"), Is(p, "police officer")}).

  wff18!:  all(p)(Person(p) => (andor(0,1){Is(p,police officer),Is(p,chef)}))    

 CPU time : 0.01 

: ;;;
;;; jp: Question: Who holds which jobs?
Is(?p, ?j)? (8 0)

  wff108!:  Is(Thelma,boxer)    
  wff107!:  ~Is(Thelma,guard)    
  wff105!:  ~Is(Thelma,teacher)    
  wff103!:  ~Is(Pete,boxer)    
  wff101!:  ~Is(Pete,guard)    
  wff98!:  Is(Pete,telephone operator)    
  wff96!:  Is(Pete,actor)    
  wff95!:  ~Is(Steve,boxer)    
  wff93!:  ~Is(Steve,guard)    
  wff91!:  ~Is(Steve,teacher)    
  wff89!:  ~Is(Steve,telephone operator)    
  wff87!:  ~Is(Steve,actor)    
  wff84!:  Is(Steve,nurse)    
  wff82!:  Is(Roberta,guard)    
  wff80!:  Is(Roberta,teacher)    
  wff78!:  ~Is(Thelma,police officer)    
  wff76!:  ~Is(Steve,chef)    
  wff75!:  ~Is(Pete,chef)    
  wff72!:  ~Is(Roberta,nurse)    
  wff71!:  ~Is(Roberta,actor)    
  wff70!:  ~Is(Roberta,telephone operator)    
  wff69!:  ~Is(Thelma,nurse)    
  wff68!:  ~Is(Thelma,actor)    
  wff67!:  ~Is(Thelma,telephone operator)    
  wff32!:  Is(Thelma,chef)    
  wff28!:  Is(Steve,police officer)    
  wff23!:  ~Is(Roberta,chef)    
  wff22!:  ~Is(Roberta,police officer)    
  wff21!:  ~Is(Pete,nurse)    
  wff20!:  ~Is(Pete,police officer)    
  wff19!:  ~Is(Pete,teacher)    
  wff10!:  ~Is(Roberta,boxer)    

 CPU time : 0.50 

: ;;;
;;; Tell me the eight positive answers you figured out.
Is(?p, ?j)??

  wff28!:  Is(Steve,police officer)    
  wff32!:  Is(Thelma,chef)    
  wff80!:  Is(Roberta,teacher)    
  wff82!:  Is(Roberta,guard)    
  wff84!:  Is(Steve,nurse)    
  wff96!:  Is(Pete,actor)    
  wff98!:  Is(Pete,telephone operator)    
  wff108!:  Is(Thelma,boxer)    

 CPU time : 0.00 

: 

End of /projects/snwiz/Install/Sneps-2.7.0/demo/snepslog/jobspuzzle.snlog demonstration.


 CPU time : 0.56