home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / ai / 5079 < prev    next >
Encoding:
Internet Message Format  |  1993-01-23  |  2.9 KB
  1. Xref: sparky comp.ai:5079 comp.ai.neural-nets:5006 sci.logic:2651
  2. Path: sparky!uunet!news.univie.ac.at!scsing.switch.ch!univ-lyon1.fr!ghost.dsi.unimi.it!rpi!usc!howland.reston.ans.net!spool.mu.edu!agate!doc.ic.ac.uk!warwick!uknet!bradford.ac.uk!L.Newnham
  3. From: L.Newnham@bradford.ac.uk (Leonard Newnham)
  4. Newsgroups: comp.ai,comp.ai.neural-nets,sci.logic
  5. Subject: Re: Neural Network Controlled Theorem Proving
  6. Message-ID: <1993Jan27.154329.20411@bradford.ac.uk>
  7. Date: 27 Jan 93 15:43:29 GMT
  8. Organization: University of Bradford, UK
  9. Lines: 71
  10. Originator: 90908502@muser
  11. Nntp-Posting-Host: muser
  12.  
  13. I wrote: 
  14. > I am doing research into temporal logic theorem proving.  I am thinking
  15. > of using a neural network as a method of learning useful heuristics
  16. > to control the direction of the search.  The basic idea is that the
  17. > neural network learns to recognise patterns in the theorem to be
  18. > proved that enable the theorem prover to proceed in an efficient manner
  19. > towards a proof.
  20. > 
  21. > I am familiar with the 2 or 3 papers Ertel and Suttner have published 
  22. > in this area but have, so far, not been able to find any other research 
  23. > along similar lines.
  24. > 
  25. > I would be most grateful if anyone could point me in the direction of
  26. > any other research in this area.
  27. > 
  28. > Please email and I will post a summary.
  29.  
  30.  
  31. Well from several replies I have compiled the following set of
  32. references:
  33.  
  34. TI: REPRESENTING HEURISTIC-RELEVANT INFORMATION FOR AN AUTOMATED THEOREM
  35.     PROVER
  36. AU: SUTTNER_CB
  37. SO: ASPECTS AND PROSPECTS OF THEORETICAL COMPUTER SCIENCE 1990 VOL.464
  38.     C26 PP.261-270
  39.  
  40. TI: REPRESENTING HEURISTIC-RELEVANT INFORMATION FOR AN AUTOMATED THEOREM
  41.     PROVER
  42. AU: SUTTNER_CB
  43. JN: LECTURE NOTES IN COMPUTER SCIENCE 1990 VOL.464 PP.261-270
  44.  
  45. Suttner C, B. and Ertel W.  Using Back-Propagation for guiding the
  46. search of a theorem prover, International Journal of Neural Networks,
  47. vol 2, part 1, 1990.
  48.  
  49. Ertel, W. et al.  Learning heuristics for a Theorem Prover using Back
  50. Propagation, Procs of the 5th OGAI Conf., 1989.
  51.  
  52. A. Ultsch, R. Hannuschka, U. Hartmann, and V. Weber, "Learning of Control
  53. Knowledge for Symbolic Proofs with Backpropagation Networks", Parallel
  54. Processing in Neural Systems and Computers, Elsevier Science Publishers
  55. B.V. (North Holland), 1990.
  56.  
  57. A. Ultsch, R. Hannuschka, U. Hartmann, M. Mandischer, and V. Weber,
  58. "Optimizing Logical Proofs with Connectionist Networks", Proceedings
  59. of the International Conference on Artificial Neural Networks", 1991.
  60.  
  61.  
  62. In German:
  63.  
  64. Suttner, C. B. Learning Heuristics for Automatic Theorem Proving,
  65. Diploma Thesis, Technical University Munich. 1989.
  66.  
  67. Goller, C.  Name not known, Diploma Thesis, Technical University Munich.
  68.  
  69.  
  70. As far as I am aware there is no research in progress.  However, Goller 
  71. and Ertel are planning to resume work once funding is obtained.
  72.  
  73.  
  74. If anyone can add to this list please let me know.
  75.  
  76. -- 
  77.  
  78. Leonard               e-mail:  L.Newnham@bradford.ac.uk
  79.  
  80. -- 
  81.  
  82. Leonard               e-mail:  L.Newnham@bradford.ac.uk
  83.