home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2170 < prev    next >
Encoding:
Internet Message Format  |  1992-11-24  |  1.5 KB
  1. Path: sparky!uunet!zaphod.mps.ohio-state.edu!saimiri.primate.wisc.edu!usenet.coe.montana.edu!ogicse!psgrain!ee.und.ac.za!ucthpx!elc.mth.uct.ac.za!hardy
  2. From: hardy@elc.mth.uct.ac.za (Hardy Hulley)
  3. Newsgroups: sci.logic
  4. Subject: Re: Looking for proof checking/building software for teaching
  5. Message-ID: <1992Nov23.234310.28222@ucthpx.uct.ac.za>
  6. Date: 23 Nov 92 23:43:10 GMT
  7. Article-I.D.: ucthpx.1992Nov23.234310.28222
  8. References: <45@beech.ukc.ac.uk>
  9. Sender: news@ucthpx.uct.ac.za (UCT News Admin.)
  10. Organization: University of Cape Town
  11. Lines: 27
  12. X-Newsreader: Tin 1.1 PL4
  13.  
  14. sjt@ukc.ac.uk (S.J.Thompson) writes:
  15. : I am looking for software to support teaching propositional and predicate
  16. : logic at undergraduate level. Specifically, I would like software for the
  17. : IBM PC or for Sun workstations which support the interactive construction of
  18. : proofs. I will post a summary of responses, assuming I receive any, to the
  19. : net.
  20. : 
  21. : Many thanks
  22. : 
  23. : Simon Thompson
  24.  
  25. Last year we wrote a very simple Predicate Calculus proof-checker which runs
  26. on top of Cambridge University's HOL theorem prover. We had exactly the same
  27. idea as you have - we got undergraduate students to construct their proofs
  28. in the system, and the proof-checker then checked the validity of these proofs.
  29.  
  30. The HOL software runs beautifully on a Sun workstation, and writing a system
  31. especially for Predicate Calculus is a simple exercise.
  32.  
  33. Hardy Hulley
  34.  
  35. Lab. for Formal Aspects and Complexity in Computer Science
  36. University of Cape Town
  37.  
  38.  
  39.  
  40.  
  41.