- From: pat hayes <phayes@ai.uwf.edu>
- Date: Tue, 20 Mar 2001 16:57:37 -0600
- To: jos.deroo.jd@belgium.agfa.com
- Cc: www-rdf-logic@w3.org
> > [Pat] > > You talk above about a PROOF of C from A->B and B->C, which I guess > > I don't understand since C doesnt follow from those two premises. Do > > you mean a proof of C from those two implications plus the assumption > > A? > >definitely (I should also sleep more instead of giving half-baken replies;-) > > > That would go > > A + A->B ==> B + B->C ==> C > > using forward reasoning. Written as resolution and using backward > > inference, it would be > > > > C-> B->C > > ------------ > > B-> A->B > > --------------- > > A-> ->A > > --------------- > >Are you suggesting a notation for the ------------ or the above ==> ? >Is it something like *log:entails* or what could it be (and fitting >with http://www.w3.org/DesignIssues/Notation3.html )? I was just (informally) trying to indicate the sequence of applying rules of inference. They are often written with premises above the line, conclusions below. The -> notation for clauses follows Prolog usage, where one 'negates' an atom (or queries it) by saying that it implies nothing (=false in a disjunction, ie a clause), so ' C->' means 'not C', and the backward search terminates with a null clause (which I should really have written as the conclusion '->') Its not really log:... anything, since its not an expression but more like a step in a process. One can think of inference rules as things that add sentences to proofs, and then the proof can itself be seen as a kind of execution trace of the process by which it was built, structured so as to demonstrate the validity of the sentence. This is quite a neat way to think about proofs in general, actually. Pat Hayes Pat Hayes --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes
Received on Tuesday, 20 March 2001 17:56:03 UTC