W3C home > Mailing lists > Public > public-rif-wg@w3.org > March 2006

RE: [UCR] RIF needs different reasoning methods

From: <jos.deroo@agfa.com>
Date: Mon, 6 Mar 2006 22:40:39 +0100
To: wagnerg@tu-cottbus.de
Cc: "'Bijan Parsia'" <bparsia@isr.umd.edu>, "'Francois Bry'" <bry@ifi.lmu.de>, public-rif-wg@w3.org, public-rif-wg-request@w3.org
Message-ID: <OF1DB28021.3DB9B4D1-ONC1257129.00757F65-C1257129.0077105A@agfa.com>

[just a quick thanks]
>> > Isn't resolution a refutation technique? Did you mean 
>> > something stronger?
>> REsolution (including SL resolution) are refuytartion methods. SLD
>> resolution is not - in spite of a common belief.
> Francois is pointing to the fact that SLD resolution corresponds 
> "isomorphically" to constructive inference based on Modus Ponens.
> Therefore, it's not really refutation-based.

Thanks Gerd for pointing this out; I still learn so much
and was kind of just doing this for many years without
realizing; indeed the kind of proof structures that I get
from instrumenting an SLD type of reasoning is just GMP
i.e. in a Reverse Polish Notation style compact proof (*)
"push the facts, pop the antecedents and push the conclusions". 

Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

(*) e.g. the "body" tuples of the objects with "head":"GND"
in http://eulersharp.sourceforge.net/2006/02swap/graph.html
Received on Monday, 6 March 2006 21:41:07 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:47:37 UTC