- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Mon, 9 Apr 2001 02:40:59 +0100
- To: phayes@ai.uwf.edu
- Cc: www-rdf-logic@w3.org, aswartz@swartzfam.com
> >When using resolution one cannot have such p->false rules. > > Incorrect. In fact, resolution REQUIRES the use of such clauses. Of course it requires the use of such clauses, but only ONE such clause, namely for the goal to be proved > >So one cannot (as such) deny the fact that p is true. > > Yes, one can. If one could not deny it, resolution could never find a > contradiction. I could see the use of negation in the premises of rules but not as false :- p rules in a prolog program for instance maybe I'm missing something in my knoledge of resolution ... > >There is however an easier problem (maybe). > >On the proof level (where proof expressions live) > >we can discover that p has a no-proof-found value. > >Of course that is not the denial of p but that > >is not a problem for a proof expressions's life! > >All it has to express is evidence that can be > >syntactically checked to give semantic validity > >(and such expressions can contain p->false > >parts coming from negated premisses). > > I have no idea what you are talking about in the above paragraph. Can > you rephrase it? In particular, what is the 'proof level' ? The proof level is what TimBL has drawn so nicely in http://www.w3.org/2001/Talks/0228-tbl/slide5-0.html I will rephrase my points later (I really have to sleep now ...) (and really sorry for any confusion) -- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Sunday, 8 April 2001 20:41:11 UTC