alessandro-montanari / tuprolog

Automatically exported from code.google.com/p/tuprolog
0 stars 0 forks source link

A == B succeeds when it should fail (tuProlog 2.6) #18

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
Original bug report from 2008, still applicable up to tuProlog 2.6

I encountered this problem while modifying the PTTP prover 
(http://www.ai.sri.com/~stickel/pttp.html) to run with tuProlog. I am attaching 
a JUnit file that has been simplified as much as possible. The resulting code 
is slightly intermittent; I have to run it twice to get the error to occur, but 
then it consistently occurs (does the JVM "remember" something from the first 
run?). I also found that making trivial changes to the theory would cause the 
error to disappear; perhaps this is related to the intermittency.
The problem occurs in line 72 of the JUnit file where two uninstantiated 
variables are being compared, L1 == L2.
The problem seems to be in the Var.isEqual() method. By adding a check of the 
variable's completename as well as its timestamp, the problem went away.
(I am coming to appreciate your design for tuProlog more and more. Perhaps I 
will be able to provide a 2p Prover Library that implements some of Stickel's 
suggestions for speeding up PTTP.)
I am running 2p-2.1 under Windows XP SP2 and J2SE 1.5.

COMMENT:
seemed solved (E.Signorin, May 2013), but occasionally the problem seems to 
re-appears. To be further investigated.

Original issue reported on code.google.com by enrico.d...@gmail.com on 6 Dec 2013 at 1:23

Attachments: