search

proofcert / checkers

This is not a game.
3 stars 2 forks source link

checkers fails to backtrack to correct branch #12

Open shaolintl opened 7 years ago

shaolintl commented 7 years ago

Using ELPI in the gandalf2017 branch, when running: ./prover-elpi.sh modtab-min-1

we get the following attached files min.txt max.txt

The problem is that in max.txt we store lind (lind eind) and decide on it In min.txt we store lind (lind X) but we never decide on something of the form lind (lind _) instead, we keep trying the same ones over and over again:

+++ dec inCtxt (lind (rind (lind X0))) (p (q1 x5)) +++ dec inCtxt relind (n (rel zero x5)) +++ dec inCtxt (rind (lind X0)) (d+ (all x6 \ n (rel zero x6) !-! p (q1 x6)))

shaolintl commented 7 years ago

the text in the file shows only storing and deciding. I removed the rest

shaolintl commented 7 years ago

Same problem also with Teyjus, see attached files. So the problem is in our program. Maybe we should introduce some cuts. max2.txt min2.txt

shaolintl commented 7 years ago

I think I have found the problem. It seems to be related to the fact that we dont place a decide bound when we dont use a decision tree. The result is that some decides, such as on forall, are happening infinitely often. The solution is to place a decide bound on at least the forall, and probably on all formulas. The number might be that we can use the diamond box relation to see how many times we might need to decide?

emmevolpe commented 7 years ago

Yes. I think we can set a bound related to the formula to prove. Why is the \forall worse than the other operators?

shaolintl commented 7 years ago

I am not sure if it is worse. The decide entered a loop when it encountered the forall. Instead of failing on the branch, it just decided again. It didnt happen for the other decided formulas.

shaolintl commented 7 years ago

@emmevolpe What do you think should be the decide depth? One for all formulas except exists which we determine according to the diamond-box relation in the certificate?

shaolintl commented 7 years ago

@emmevolpe waiting for your reply for the above. Right now, the value is fixed to 2 for all nodes which is enough for the example. The example is running through now with a variable for the decide tree.