log:forAll makes sense? [was: Can we agree on triples ?]

"Peter F. Patel-Schneider" wrote:
[...]
>  For
> example, if you represent quantification using "http://www.bar.com/logic#forall",
> you could end up with triples of the form
> 
>         {http://www.bar.com/logic#forall,a,b}
> 
> which should not result in the assertion that there is some forall
> relationship between the representation of the variable a and the
> representation of the formula b,

I wonder about that...

> at least not one that will commingle with
> assertions that come from triples of the form
> 
>         {loves,john,mary}

Er... why not? That's pretty much the design TimBL has coded up[swap].
I've been trying to convince myself alternatively that is
or is not a sound design. Maybe you can settle this for me/us...

Looking at it in KIF, the latter is:

	(loves john mary)

and the former is, say,

	(log:forall '?a '(loves ?a mary))

where log:forall is defined so that this expands to

	(wtr '(forall (?a) (loves ?a mary)))

I'm not sure how TimBL's design gets from a to 'a
in the forall bit, but it seems to.

Tim, can you explain why you don't need to
quote the last occcurence of :a in the N3 way
of doing quantification?

	{ :a :loves :mary } a log:Truth; log:forAll :a.

[swap] http://www.w3.org/2000/10/swap/

There's some difference between the {} mechanism
in N3 and KIF's quoting and wtr that I can't figure out.
When I looked at KIF and RDF, I couldn't work out
all the quoting issues.

  http://www.w3.org/2000/07/hs78/KIF

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/