Path: utzoo!attcan!utgpu!bnr-vpa!bnr-fos!bnr-di!anv
From: anv@bnr-di.UUCP (Andre Vellino)
Newsgroups: comp.lang.prolog
Subject: Re: Propositional Theorem Prover
Message-ID: <158@bnr-di.UUCP>
Date: 24 May 89 15:43:29 GMT
References: <1663@kulcs.kulcs.uucp>
Organization: DI, Bell-Northern Research, Ottawa, Ont.
Lines: 43




Bart Demoen is quite right: my conclusion wasn't strong enough.  
What I should have concluded was that the C vs. Prolog debate had 
not been fair to Prolog.  Correct me if I am wrong, but I believe the C 
program was written first and the algorithm that it implemented, 
data-structures and all, were then translated into Prolog (with a 
not-terribly surprising drop in performance).  This didn't seem to me 
to be the right approach for comparing languages: Prolog is bound to 
lose in this sort of comparison if only because of the extra overhead.  

It seems to me that if you are going to compare two programming 
languages so as to provide reasons for preferring one to the other, 
you should measure how they compare at solving the same 
*problems*, not which performs faster with the same algorithm and 
the same data structures.  This is especially true when comparing 
two programming languages with different conceptual models.

In fact, what my little program really shows is that the improved 
analytic tableau method has a smaller search space (for some 
examples anyway) than set-of-support resolution (which spends a lot 
of its time doing useless subsumption checking).  But the point is, by 
Bart Demoen's own admission, one is more likely to discover this 
tableau method by thinking about how best to solve the problem in 
Prolog (and come up with a 6-line program) than one is to come up 
with a (60-line) C program that does the same thing 5 times faster.

I should add that I have nothing against the Prolog set-of-support 
theorem prover as a benchmark for comparing Prolog systems 
against each other.  I just wanted to contest the claim that the 
problem with Prolog is that it doesn't have a destructive assignment.
---------------------------------------------------------------------
Andre Vellino
Computing Research Laborartory           TEL: (613) 763-7514
Bell-Northern Research                   FAX: (613) 763-4222
P.O. BOX 3511 Station C                  BITNET: vellino@bnr.ca
Ottawa, Ontario                          UUCP: utzoo!bnr-vpa!bnr-di!anv
Canada K1Y 4H7                                 @ ai.utoronto
-----------------------------------------------------------------------
Disclaimer: the views expressed in this article are not necessarily endorsed
	    by BNR, ... etc.