Re: KR, meet WWW. was: Clarifying what a URL identifies (Four Uses of a URL)

[...]

> I keep mulling over other approaches here, like how to do this
> (log:semantics) in backward chaining, and how to graft it into a
> resolution theorem prover.


good point; using log:conjunction and log:semantics we can write

[ is log:conjunction of
   ( [ is log:semantics of <http://www.agfa.com/w3c/euler/gedcom-relations>
]
     [ is log:semantics of <http://www.agfa.com/w3c/euler/gedcom-facts> ]
     [ is log:semantics of <http://www.w3.org/2002/07/owl> ]
     [ is log:semantics of <http://www.w3.org/2000/01/rdf-schema> ] ) ]
log:implies
     [ is log:semantics of <http://www.agfa.com/w3c/euler/gedcom-query> ] .

but we actually kind of treat that as

( <http://www.agfa.com/w3c/euler/gedcom-relations>^^log:semantics
  <http://www.agfa.com/w3c/euler/gedcom-facts>^^log:semantics
  <http://www.w3.org/2002/07/owl>^^log:semantics
  <http://www.w3.org/2000/01/rdf-schema>^^log:semantics )^^log:conjunction
log:implies
  <http://www.agfa.com/w3c/euler/gedcom-query>^^log:semantics .

and then it is quite straightforward to have such a triple
in a rule premis or in a goal and do backward chaining
we have a testcase at http://www.agfa.com/w3c/euler/etc5
and its proof at http://www.agfa.com/w3c/euler/etc5-proof.n3


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