worries about useMentionOp and how queries relate to rules and proofs

Pat,

I can't quite put my finger on it, but I'm afraid there are
some serious architectural use/mention issues with operators like
BOUND, URI-equal, isURI, and isBlank
  http://www.w3.org/2001/sw/DataAccess/issues#useMentionOp

As I see the architecture, a query plays the role of
a conjecture to be proved. A query solution is a sketch
of a proof.

If I write

 SELECT ?who
 WHERE ?who foaf:name "Dan Connolly"

it's akin to asking a theorem prover to prove:

  exists (x) such that foaf:name(x, "Dan Connolly")

The solution "?who binds to <danshomePage#topic>"
is a sketch of a proof (I think the literature
uses the term "witness" for this sort of thing).

Now I can't imagine how to turn

 SELECT ?who
 WHERE ?who foaf:homePage ?x
   AND isURI(?x)

into a conjecture to be proved by a theorem prover.
isURI() is not a function of objects in the
domain of discourse, but an operator that distinguishes
one sort of term from another. We might have

	<dansHomePage#topic> owl:sameAs _:somebody .
and by definition
	isURI(<dansHomePage#topic>)
but not
	isURI(_:somebody)

This sets off flags in my mind, but I can't state,
in black-and-white, testable ways that matter to
applications and coders, why it matters.

Does it worry you?


p.s. formally this is a WG issue
  http://www.w3.org/2001/sw/DataAccess/issues#useMentionOp
In Helsinki, we has some relevant discussion and made
a nearby decision, but it wasn't explicitly a decision
to close this issue.

  RESOLVED: BOUND keyword and no UNSAID to address common
  UNSAID issues. KendallC abstaining
  http://www.w3.org/2001/sw/DataAccess/ftf4.html#item04

I'm trying to figure out whether to open substantive discussion
of this useMentionOp issue or just say "oh... yeah, we meant to close
that one too, didn't we?"



-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Friday, 4 February 2005 00:39:27 UTC