gilith/metis

BUG found in metis program

giomasce opened this issue · 5 comments

giomasce commented

When launching metis with the following problem made of just one line:

fof(1,conjecture,(((Y=Z=>((X=Y=>p(X,Y,Z))&?[X]:(X=Y&p(X,Y,Z))))&?[Y]:(Y=Z&((X=Y=>p(X,Y,Z))&?[X]:(X=Y&p(X,Y,Z)))))<=>((Y=Z=>((X=Z=>p(X,Y,Z))&?[X]:(X=Z&p(X,Y,Z))))&?[Y]:(Y=Z&((X=Z=>p(X,Y,Z))&?[X]:(X=Z&p(X,Y,Z))))))).

I obtain this result:

FATAL ERROR: BUG found in metis program:
cumulativeCounts: c1 = (+1.09861228867,-1.09861228867), c2 = (+1.09861228867,-1.38629436112)

I do not have much experience with metis or ATPs in general, so I cannot help much, but since metis itself is declaring a bug, I thought that I might be helpful to report.

gilith commented

Hi Giovanni,

Thank you for the bug report. I'd like to reproduce it, but so far have not been able to:

$ cat bug.tptp
fof(1,conjecture,(((Y=Z=>((X=Y=>p(X,Y,Z))&?[X]:(X=Y&p(X,Y,Z))))&?[Y]:(Y=Z&((X=Y=>p(X,Y,Z))&?[X]:(X=Y&p(X,Y,Z)))))<=>((Y=Z=>((X=Z=>p(X,Y,Z))&?[X]:(X=Z&p(X,Y,Z))))&\
?[Y]:(Y=Z&((X=Z=>p(X,Y,Z))&?[X]:(X=Z&p(X,Y,Z))))))).
$ metis -v
metis 2.4 (release 20180301)
$ metis bug.tptp
% SZS status Theorem for bug.tptp
$

Are you running the latest version of Metis from this repo (which should be the same as the latest release)? Or is there some other difference you can think of?

Cheers,

Joe

giomasce commented

Hello,

I just realized that the bug manifests itself only when compiling with polyml. If I compile with mlton, the file is processed correctly. Maybe this is what explains the different behaviour (the Metis version is indeed the 2.4, and the git repository is up-to-date). Knowing very little of Standard ML, I had not considered this variable when first opening the issue.

At this point, I am satisfied with closing the issue without further work. I leave it to you to decide whether the bug with polyml has to be fixed or not.

Thanks, Giovanni.

gilith commented

Hi Giovanni,

That's interesting, and it seems to also depend on the version of polyml because I can't reproduce it with my installed version either, which is as follows:

$ dpkg-query -s polyml
Package: polyml
Status: install ok installed
Priority: extra
Section: interpreters
Installed-Size: 14777
Maintainer: Debian Science Maintainers <debian-science-maintainers@lists.alioth.debian.org>
Architecture: amd64
Multi-Arch: foreign
Version: 5.6-8

In the interest of tracking these kind of issues, which platform and version of polyml are you using?

Cheers,

Joe

giomasce commented

I am using an up-to-date Debian unstable on amd64. I suppose that you are using Debian stable; in case you want to go deeper, you might find the tool schroot useful (https://wiki.debian.org/Schroot) to install an independent Debian unstable system inside yours. I am of course available for helping, but as I said I know nothing of Standard ML, so I would not know what to do. Maybe tomorrow I can try to do the same test in a stable schroot.

$ dpkg-query -s polyml
Package: polyml
Status: install ok installed
Priority: optional
Section: interpreters
Installed-Size: 17995
Maintainer: Debian Science Maintainers <debian-science-maintainers@lists.alioth.debian.org>
Architecture: amd64
Multi-Arch: foreign
Version: 5.7.1-1

Thanks again, Giovanni.

gilith commented

Hi Giovanni,

You are correct that I'm using Debian stable. I don't have the expertise (or bandwidth) to investigate this issue any deeper, but the existence of a floating point arithmetic consistency check failure in this version of Poly/ML might be a useful datapoint for the developers (e.g., @dcjm).

Thanks again for the bug report, I'm going to close this issue now.

Cheers,

Joe