Blank node quantification

Hi all,

here's a crazy idea. I am not even sure I like it myself, but I wanted 
to ear others' opinion about it.

During our last call, William made a point, with which I agree (assuming 
I understood it correctly). To sum it up: people use blank node in data 
more as "local" identifiers than as proper existential variables. This 
pleads for quantifying blank nodes at the top level.

On the other hand, as we also pointed out during the call, blank nodes 
as used in rule bodies (and rule heads, I believe) need to be quantified 
locally.

Hence my crazy idea: why not make the scope of blank node determined by 
the log:implies (=>) predicate?

More precisely:

* a formula that is the subject or object of log:implies defines a new 
scope for blank nodes

* any other formula inherits the scope of its immediate parent

* blank nodes in the top level scope are quantified *before* universals 
(which is consistent with viewing them as "local constants")

Below is a long (apologies) list of examples.

WDYT?

   pa


Examples 1:

     :alice :belives { [] a :Unicorn }.
     [] a :Person.

is equivalent to (using old-style explicit quantifiers)

    @forSome v:u, v:p.
    :alice :belives { v:u a :Unicorn }.
    v:p a :Person.

----

Example 2:

     { [] a :Unicorn } => { :world a :MagicalPlace }.

is equivalent to (using old-style explicit quantifiers)

     { @forSome v:u. v:u a :Unicorn } => { :world a :MagicalPlace }.

(i.e. no change with today's interpretation)

----

Example 3:

     { ?x a :Person } => { ?x :mother [] }.

is equivalent to (using old-style explicit quantifiers)

     { ?x a :Person } => { @forSome v:m. ?x :mother v:m }.

(i.e. no change with today's interpretation)

----

Example 4:

     :alice :belives { [] a :Unicorn }.
     { ?x :believes { [] a :Unicorn } } => { ?x a :GulliblePerson }.

is equivalent to (using old-style explicit quantifiers)

     @forSome v:u1.
     :alice :believes { v:u1 a :Unicorn }.
     { @forSome v:u2. ?x :believs { v:u2 a :Unicorn } } => { ?x a 
:GulliblePerson }.

which, unless I am mistaken, is also equivalent to

     @forSome v:u1.
     :alice :believes { v:u1 a :Unicorn }.
     { ?x :believs { ?u2 a :Unicorn } } => { ?x a :GulliblePerson }.

I would expect this to produce.

     :alice a :GulliblePerson.

----

Example 5:

     :alice :belives { [] a :Unicorn }.
     { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.

is equivalent to (using old-style explicit quantifiers)

     @forSome v:u1.
     :alice :believes { v:u1 a :Unicorn }.
     { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.

I would have no problem with this producing

     :alice :wishesToRide v:u1.  # where v:u1 is still quantified by the 
top @forSome