It Is A Mystery…

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

• Global universal quantification:

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

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

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

• Global existential quantification:

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

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

  Therefore the above entails no additional statements.

• LHS universal quantification:

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

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

  Therefore the above entails no additional statements.

• LHS existential quantification:

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

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

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

• RHS universal quantification:

  @prefix : <#> .
  
  { :someValue :a :b . } => { @forAll   .   :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   .   :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 opularPerson” and, “any foaf:Person that is foaf:knows of all (known) foaf:Persons in a opularPerson” can’t be done properly without completely closing the world. cwm cannot do this without artificially closing the world through built-ins.