home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / sci / logic / 2008 < prev    next >
Encoding:
Text File  |  1992-11-12  |  1.5 KB  |  62 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!mcsun!news.funet.fi!cs.joensuu.fi!jlavi
  3. From: jlavi@cs.joensuu.fi (Jarkko Lavinen)
  4. Subject: Re: Programs for simple logic proofs: where are they?
  5. Message-ID: <1992Nov12.103723.24842@cs.joensuu.fi>
  6. Organization: University of Joensuu
  7. References: <4804@equinox.unr.edu>
  8. Date: Thu, 12 Nov 1992 10:37:23 GMT
  9. Lines: 51
  10.  
  11. mjb@dws014.unr.edu (Mike Brown) writes:
  12.  
  13. >I am looking for programs that will do proofs like:
  14. >            Prove: Q            \
  15. >    1 P then Q    Premis               > The problem
  16. >    2 P        Premis              /
  17. >    3 Q             1, 2, Modus Ponens  >  The program's proof
  18.  
  19. >(The proofs do get more involved)
  20. Isn't this just what a theorem prover does? You could try for example
  21. Otter which is available in ANL.
  22.  
  23. ----- OTTER 2.2, July 1991 -----
  24. The job began on cs, Thu Nov 12 12:32:19 1992
  25. The command was "otter".
  26.  
  27. set(binary_res).
  28. set(factor).
  29. assign(stats_level,1).
  30.  
  31. list(usable).
  32. 1 [] -P | Q.
  33. 2 [] P.
  34. end_of_list.
  35.  
  36. list(sos).
  37. 3 [] -Q.
  38. end_of_list.
  39.  
  40. given clause #1: (wt=1) 3 [] -Q.
  41. ** KEPT: 4 [binary,3,1] -P.
  42.  
  43. ----> UNIT CONFLICT at   0.01 sec ----> 5 [binary,4,2] .
  44.  
  45. Level of proof is 1, length is 1.
  46.  
  47. ---------------- PROOF ----------------
  48.  
  49. 1 [] -P | Q.
  50. 2 [] P.
  51. 3 [] -Q.
  52. 4 [binary,3,1] -P.
  53. 5 [binary,4,2] .
  54.  
  55. ------------ end of proof -------------
  56.  
  57. So You just insert premises in axioms and deny the conclusion, theorem
  58. prover then finds a contradiction. You can find the software
  59. from 140.221.10.1 = anagram.mcs.anl.gov.
  60.  
  61. >Mike Brown, mjb@cs.unr.edu    "I am the scratch monkey"
  62.