Path: utzoo!attcan!uunet!mcvax!prlb2!kulcs!bimbart From: bimbart@kulcs.uucp (Bart Demoen) Newsgroups: comp.lang.prolog Subject: Re: Propositional Theorem Prover Message-ID: <1663@kulcs.kulcs.uucp> Date: 19 May 89 06:45:08 GMT Reply-To: bimbart@kulcs.UUCP (Bart Demoen) Organization: Katholieke Universiteit Leuven, Dept. Computer Science Lines: 30 To my surprise, I have not yet seen any reply to the contribution of Andre Vellino <157@bnr-di.UUCP> (perhaps because American people do not bother to distribute their contribution to Europe) Let me quote Andre Vellino's conclusion: > What this may illustrate is that while a procedural language like C > probably lends itself well to deterministic algorithms like set-of- > support resolution, Prolog is better suited to non-deterministic > semantic techniques. If 'better suited' means that you can't write a faster C program implementing the same non-deterministic algorithm, then this is wrong: I have a 60 line C program without tricks that is 5 times faster than the Prolog program presented by Andre Vellino. I must admit though that my knowledge of what the WAM does to the Prolog program, helped me in writing the C version. If 'better suited' just means that it is easier to program in Prolog than in C, then the article was an overkill: to arrive at this conclusion, there was no need to have a non-deterministic theoremprover in Prolog that could perform a certain proof FASTER than deterministic theoremprover in C ! I think the conclusion should have been that deterministic algorithms perform better on some problems and non-deterministic algorithms perform better on other problems ... which isn't new either. The Prolog program can be sped up by a factor of 2 easely by changing the representation of the formulas and by a small folding exercise. bimbart@kulcs