home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / sci / logic / 2009 < prev    next >
Encoding:
Text File  |  1992-11-12  |  3.2 KB  |  135 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!pipex!warwick!pavo.csi.cam.ac.uk!jg
  3. From: jg@cl.cam.ac.uk (Jim Grundy)
  4. Subject: Re: Programs for simple logic proofs:  where are they?
  5. Message-ID: <1992Nov12.120607.8601@infodev.cam.ac.uk>
  6. Sender: news@infodev.cam.ac.uk (USENET news)
  7. Nntp-Posting-Host: razorbill.cl.cam.ac.uk
  8. Reply-To: jg@cl.cam.ac.uk
  9. Organization: Cambridge Hardware Verification Group
  10. References: <4804@equinox.unr.edu>
  11. Date: Thu, 12 Nov 1992 12:06:07 GMT
  12. Lines: 121
  13.  
  14. In article <4804@equinox.unr.edu>, mjb@dws014.unr.edu (Mike Brown) writes:
  15. |> I am looking for programs that will do proofs like:
  16. |>             Prove: Q            \
  17. |>     1 P then Q    Premis               > The problem
  18. |>     2 P        Premis              /
  19. |>     3 Q             1, 2, Modus Ponens  >  The program's proof
  20. |> 
  21. |> (The proofs do get more involved)
  22. |> 
  23. |> I have looked around, but can't find a program for this.
  24. |> (I tried archie searches for many keywords and didn't find a program)
  25. |> 
  26. |> Is there a program out there that will do these proofs?
  27. |> 
  28. |> Thanks
  29. |> --
  30. |> Mike Brown, mjb@cs.unr.edu    "I am the scratch monkey"
  31.  
  32. You can do this in the HOL theorem prover (several ways).
  33.  
  34. * 1: Backward Proof.
  35.  
  36. $ hol
  37.  
  38.  
  39. ===============================================================================
  40.          HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
  41. ===============================================================================
  42.  
  43. #set_goal (["P ==> Q"; "P:bool"], "Q:bool");;
  44. "Q"
  45.     [ "P" ]
  46.     [ "P ==> Q" ]
  47.  
  48. () : void
  49.  
  50. #e (MP_TAC (ASSUME "P:bool"));;
  51. OK..
  52. "P ==> Q"
  53.     [ "P" ]
  54.     [ "P ==> Q" ]
  55.  
  56. () : void
  57.  
  58. #e (ACCEPT_TAC (ASSUME "P ==> Q"));;
  59. OK..
  60. goal proved
  61. . |- P ==> Q
  62. .. |- Q
  63.  
  64. Previous subproof:
  65. goal proved
  66. () : void
  67.  
  68. #quit ();;
  69. Bye.
  70. $
  71.  
  72. * 2: Forward Proof
  73.  
  74. $ hol
  75.  
  76.  
  77. ===============================================================================
  78.          HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
  79. ===============================================================================
  80.  
  81. #top_print print_all_thm;;
  82. - : (thm -> void)
  83.  
  84. #let th1 = ASSUME "P ==> Q";;
  85. th1 = P ==> Q |- P ==> Q
  86.  
  87. #let th2 = ASSUME "P:bool";;
  88. th2 = P |- P
  89.  
  90. #let th3 = MP th1 th2;;
  91. th3 = P ==> Q, P |- Q
  92.  
  93. #quit ();;
  94. Bye.
  95. $
  96.  
  97. * 3: Let HOL do a backward proof for you.
  98.  
  99. $ hol
  100.  
  101.  
  102. ===============================================================================
  103.          HOL88 Version 2.01 (Sun4/AKCL), built on 20/10/92
  104. ===============================================================================
  105.  
  106. #set_goal (["P ==> Q"; "P:bool"], "Q:bool");;
  107. "Q"
  108.     [ "P" ]
  109.     [ "P ==> Q" ]
  110.  
  111. () : void
  112.  
  113. #e RES_TAC;;
  114. OK..
  115. goal proved
  116. .. |- Q
  117.  
  118. Previous subproof:
  119. goal proved
  120. () : void
  121.  
  122. #quit ();;
  123. Bye.
  124. $
  125.  
  126. ===============================================================================
  127. Jim Grundy               
  128. University of Cambridge | Phone: +44 223 334760            | This space has
  129. Computer Laboratory     | Fax:   +44 223 334678            | been intentionally
  130. New Museums Site        | Telex: CAMSPLG 81240             | left blank for
  131. Pembroke Street         | email: jg@cl.cam.ac.uk           | formatting
  132. Cambridge  CB2 3QG      |                                  | purposes.
  133. UNITED KINGDOM          |                                  |
  134. ===============================================================================
  135.