From: <jos.deroo.jd@belgium.agfa.com>

Date: Mon, 9 Apr 2001 15:08:55 +0100

To: phayes@ai.uwf.edu

Cc: www-rdf-logic@w3.org, aswartz@swartzfam.com

Message-Id: <OF69AD7DA0.2A4AC3A6-ON41256A29.003D7DCB@bayer-ag.com>

Date: Mon, 9 Apr 2001 15:08:55 +0100

To: phayes@ai.uwf.edu

Cc: www-rdf-logic@w3.org, aswartz@swartzfam.com

Message-Id: <OF69AD7DA0.2A4AC3A6-ON41256A29.003D7DCB@bayer-ag.com>

> >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' ? I see that our phrasing is indeed ussuming a lot of implicit things ... The proof level is what TimBL has drawn so nicely in http://www.w3.org/2001/Talks/0228-tbl/slide5-0.html We also assume a proof expression to be a propositional logic formula. Of course this is not yet a proof language! Such a proof can be the result of e.g. predicate logic inferences (using e.g. binary predicate reflexive resolution, but of course there are many, many proof engine technologies). I want to refer here to the stuff that we have exemplified at http://www.agfa.com/w3c/euler/ (just to fix the idea). In there the so called proofs are nested material implications. If those proofs are posed as a new lemma one obtains a so called checked proof (which is actually a fixpoint when also posed as a lemma). A checked proof is somehow giving the syntactic validity axioms |- lemma and as we know from symbolic logic syntactic validity |- implies semantic validity |= (but not necessarily the other way around according to an interpretation of Goedel's incompleteness theorem). Proof checking is indeed a straightforward thing (certainly compared to proof generation) and if no proof could be generated, the proof check of that will be even simpler ... -- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/Received on Monday, 9 April 2001 09:09:05 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:52:38 GMT
*