Quantifying cwm Variables…

Mostly for my benefit, but here are a few examples of how cwm’s N3Rules translate into formal logic:

  • Global universal quantification:

    @prefix : <#> .
    @forAll :x  .
    
    { :x  :a :b . } => { :x  :c :d . } .
    
    :someValue :a :b .
    

    ∀x (a(x, b) → c(x, d))

    Therefore the above entails the additional statement :someValue :c :d . as :x is bound to :someValue on the RHS.

  • Global existential quantification:

    @prefix : <#> .
    @forSome :x  .
    
    { :x  :a :b . } => { :x  :c :d . } .
    
    :someValue :a :b .
    

    ∃x (a(x, b) → c(x, d))

    Therefore the above entails no additional statements.

  • LHS universal quantification:

    @prefix : <#> .
    
    { @forAll :x  . :x  :a :b . } => { :x  :c :d . } .
    
    :someValue :a :b .
    

    (∀x a(x, b)) → c(x, d)

    Therefore the above entails no additional statements.

  • LHS existential quantification:

    @prefix : <#> .
    
    { @forSome :x  . :x  :a :b . } => { :x  :c :d . } .
    
    :someValue :a :b .
    

    (∃x a(x, b)) → c(x, d)

    Therefore the above entails the additional statement :x :c :d . as :x is unbound on the RHS.

  • RHS universal quantification:

    @prefix : <#> .
    
    { :someValue :a :b . } => { @forAll :x  . :x  :c :d . } .
    
    :someValue :a :b .
    

    a(someValue, b) → (∀x c(x, d))

    Therefore the above entails (generally) @forAll :z . :z :c :d .

  • RHS existential quantification:

    @prefix : <#> .
    
    { :someValue :a :b . } => { @forSome :x  . :x  :c :d . } .
    
    :someValue :a :b .
    

    a(someValue, b) → (∃x c(x, d))

    Therefore the above entails the additional statement [ :c :d ] .

Finally, two trickier specific examples: “If there exists a foaf:Person that all (known) foaf:Persons foaf:know, then there exists a :P opularPerson” and, “any foaf:Person that is foaf:knows of all (known) foaf:Persons in a :P opularPerson” can’t be done properly without completely closing the world. cwm cannot do this without artificially closing the world through built-ins.

Tags: , , ,

One Response to “Quantifying cwm Variables…”

  1. Henry Story says:

    Hi, your N3 code has shows a lot of smileys in my browser (Firefox 3.5).
    Happy code, but perhaps that was not your intention.

Leave a Reply