Problems with @forAll

2009-08-30
2013-04-05
  • Hi

    I made some tests with @forAll , and I found no way to make it work.
    This used as a query :

    # this gives no result with EYE and Fuxi
    # run forever with CWM
    # @forAll :CLASS .
    # { ?CLASS :subClassOrSameClass ?CLASS . }.

    # this gives no result either with EYE and Fuxi
    @forAll :CLASS .
    { true }
    =>
    { ?CLASS :subClassOrSameClass ?CLASS . }.

    {
      :c :subClassOrSameClass :c .
    } => {
      :test :result :ok .
    } .

     
    • Jos De Roo
      Jos De Roo
      2009-08-30

      For Eye non range restricted variables are existentials
      hence for :c :subClassOrSameClass :c . no proof found.

      P.S.
      1/ don't put the :subClassOrSameClass rule in the query file
      2/ when using @forAll :X don't use ?X but :X

       
    • So, if I understand well, there is no way to express an unrestricted reflexive predicate.
      In general, in EYE the @forAll is unable to enforce the universal character of a variable that does not appear in the antecedent.
      If possible, a warning about the uselessness of the @forAll in such cases would be good .

      So , instead of :
      { true }
      =>
      { :CLASS :subClassOrSameClass :CLASS }.

      I did this which works fine :
      { :CLASS a owl;Class }
      =>
      { :CLASS :subClassOrSameClass :CLASS }.