Re: builtins, witnesses and contraint satisfaction problems

Thanks Pierre-Antoine, I agree.

As discussed in the meeting today, I took an action to change EYE so
that it just creates witnesses for unbound universals in the conclusion.
It does not matter whether those universals are range-restricted (*) or not.

The good news is that all current tests are working fine that way!

jos

-- https://josd.github.io/ <http://josd.github.io/>

(*) all variables in the conclusion necessarily occur in the premise

On Mon, Feb 8, 2021 at 7:18 PM Pierre-Antoine Champin <
pierre-antoine.champin@ercim.eu> wrote:

> 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
>
>
>