builtins, witnesses and contraint satisfaction problems

Hi all,

following our discussion during the call, I made a small experiment with 
EYE [1]

{ (?x ?y ?z) math:memberCount ?c. }
     => { :TEST1 :gave ?c }.
{ ?x math:notGreaterThan ?y. ?y math:notGreaterThan ?z. (?x ?y ?z) 
math:memberCount ?c. }
     => { :TEST2 :gave ?c }.
{ ?x math:notGreaterThan ?y. ?y math:notGreaterThan ?z. ?z 
math:notGreaterThan ?x. (?x ?y ?z) math:memberCount ?c. }
     => { :TEST3 :gave ?c }.

 From a purely logical point of view, the first two should pass.

EYE only passes the first one. And despite the fact that this is 
logically incomplete, I am quite happy with that.

My intuition is that math:memberCount only matches if the unbound 
variables in the list are not otherwise constrained, and that sounds 
like a reasonable heuristics when it comes to succeeding with unbound 
variables.

   pa


[1] 
http://ppr.cs.dal.ca:3002/n3/editor/?formula=%40prefix%20math%3A%20%3Chttp%3A%2F%2Fwww.w3.org%2F2000%2F10%2Fswap%2Fmath%23%3E.%0A%40prefix%20log%3A%20%20%3Chttp%3A%2F%2Fwww.w3.org%2F2000%2F10%2Fswap%2Flog%23%3E.%0A%40prefix%20xsd%3A%20%20%3Chttp%3A%2F%2Fwww.w3.org%2F2001%2FXMLSchema%23%3E.%0A%0A%0A%7B%20(%3Fx%20%3Fy%20%3Fz)%20math%3AmemberCount%20%3Fc.%20%7D%20%3D%3E%20%7B%20%3ATEST1%20%3Agave%20%3Fc%20%7D.%0A%7B%20%3Fx%20math%3AnotGreaterThan%20%3Fy.%20%3Fy%20math%3AnotGreaterThan%20%3Fz.%20(%3Fx%20%3Fy%20%3Fz)%20math%3AmemberCount%20%3Fc.%20%7D%20%3D%3E%20%7B%20%3ATEST2%20%3Agave%20%3Fc%20%7D.%0A%7B%20%3Fx%20math%3AnotGreaterThan%20%3Fy.%20%3Fy%20math%3AnotGreaterThan%20%3Fz.%20%3Fz%20math%3AnotGreaterThan%20%3Fx.%20(%3Fx%20%3Fy%20%3Fz)%20math%3AmemberCount%20%3Fc.%20%7D%20%3D%3E%20%7B%20%3ATEST3%20%3Agave%20%3Fc%20%7D.%0A&format=n3

Received on Monday, 8 February 2021 18:17:51 UTC