Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo

Close

existential quantification and congruence

Help
2013-11-03
2013-11-05
  • Leonid Ryzhyk
    Leonid Ryzhyk
    2013-11-03

    When running Reduce on the following input:

    load redlog;
    rlset pasf;
    phi := ex(x, cong(x+1, z, 16));
    rlqe (phi);
    

    I obtain this result:

    15*z + 14 ~16~ 0 or 15*z + 13 ~16~ 0 or 15*z + 11 ~16~ 0 or 15*z + 8 ~16~ 0
     or 15*z + 7 ~16~ 0 or 15*z + 4 ~16~ 0 or 15*z + 2 ~16~ 0 or 15*z + 1 ~16~ 0
     or 5*z + 4 ~16~ 0 or 5*z + 3 ~16~ 0 or 5*z + 2 ~16~ 0 or 5*z + 1 ~16~ 0
     or 3*z + 2 ~16~ 0 or 3*z + 1 ~16~ 0 or z + 1 ~16~ 0 or z ~16~ 0
    

    which is obviously correct; however I was hoping that Redlog would be able to simplify it all the way to "true". Is there a way to achieve this, e.g., by using a different encoding of the problem?

    Thanks!
    Leonid

     
  • Thomas Sturm
    Thomas Sturm
    2013-11-04

    Unfortunately, the simplifier is not very good.

    If you suspect that it is true, you can directly ask for it, like:

    rlqe all(z, phi);

    More conveniently you could go

    rlqe rlall phi;

    where rlall() is the universal closure, i.e. all remaining variables are universally quantified.

    Best,

    Thomas

     
    • Leonid Ryzhyk
      Leonid Ryzhyk
      2013-11-05

      Thanks for the explanation!

      Leonid