Path: utzoo!utgpu!news-server.csri.toronto.edu!mailrus!iuvax!cica!tut.cis.ohio-state.edu!zaphod.mps.ohio-state.edu!samsung!rex!ames!uhccux!munnari.oz.au!lee From: lee@munnari.oz.au (Lee Naish) Newsgroups: comp.lang.prolog Subject: Re: Hype about Prolog Message-ID: <4339@munnari.oz.au> Date: 1 Jun 90 02:38:36 GMT References: <2562@randvax.UUCP> Sender: news@cs.mu.oz.au Reply-To: lee@munmurra.UUCP (Lee Naish) Organization: Comp Sci, University of Melbourne Lines: 32 In article <2562@randvax.UUCP> narain@randvax.UUCP (Sanjai Narain) writes: > >In a sense, an executable specification is quite easy to obtain. Suppose >one can specify a problem in a formal language. Then, one can use any >complete theorem prover for it to query that specification. So, what is >to distinguish doing this in full first-order logic from doing the same in >definite clauses (with SLD-resolution)? It is the possibility of >specifying algorithmic knowledge in the latter. I am somewhat surprised that no-one has yet (to my knowledge) produced a logic program development/teaching environment which includes a decent complete theorem prover (preferably connected to a declarative debugging system). It seems like such an obvious thing to do. It allows you to to first get the logic right, then concentrate on the algorithm, using SLDNF resolution. I think this would be particularly nice for teaching purposes. We could first teach students to write specifications in logic, then explain SLDNF resolution (so they could write Prolog code which does not loop), then explain Prolog implementation (so they could write tail recursive code, not leave choice points around, etc). The testing facility in the NU-Prolog Debugging Environment goes a little way in this direction (it has a meta interpreter which uses a fair search strategy, and is connected to a declarative debugger), but the technology exists to do much better. Logic programming has a huge potential for great programming environments. Its a great shame that so few people are working on the area. lee