Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The correct way of using TPTP files with Isabe...

view this post on Zulip Email Gateway (Aug 22 2022 at 15:13):

From: Albert Berger <nbdspcl@gmail.com>
Greetings!

I'm trying to understand how to use Isabelle for proving theorems from TPTP
collection. And I haven't succeed in that.

When I call 'isabelle tptp_isabelle' with a TPTP ".p" file as an argument, I keep
getting all failures as the result. I tried 50, 600, and 6000 timeouts and the
most simple theorems.

When I first translate a TPTP file with 'isabelle tptp_translate' and after that
call 'tptp_isabelle' with the translated file, I am getting a "syntax error".

Could someone please advise the correct way of using Isabelle for solving TPTP
theorems?

Thanks.

Albert Berger.

P.S. Below are two examples of shell output for both cases.

[al isabelle ]$ TPTP=/mnt/vault/TPTP-v6.4.0 isabelle tptp_isabelle 6000 /mnt/vault/TPTP-v6.4.0/Problems/NUM/NUM005-1.p
0:00:33 elapsed time
running nitpick for 150 s
FAILURE: nitpick
running simp for 300 s
FAILURE: simp
running blast for 300 s
FAILURE: blast
running auto+spass for 600 s
FAILURE: auto+spass
running fast for 300 s
FAILURE: fast
running z3 for 150 s
FAILURE: z3
running cvc4 for 150 s
FAILURE: cvc4
running best for 150 s
FAILURE: best
running force for 300 s
FAILURE: force
running meson for 300 s
FAILURE: meson
running fastforce for 300 s
FAILURE: fastforce
running spass for 500 s
FAILURE: spass
running vampire for 500 s
FAILURE: vampire
running e for 500 s
FAILURE: e
running z3_tptp for 500 s
FAILURE: z3_tptp
running spass(1) for 250 s
FAILURE: spass(1)
running e(2) for 250 s
FAILURE: e(2)
running vampire(1) for 250 s
FAILURE: vampire(1)
running vampire(2) for 250 s
FAILURE: vampire(2)
running vampire(*) for 6000 s
FAILURE: vampire(*)
% SZS status GaveUp
poly: : warning: The type of (it) contains a free type variable. Setting it to a unique

[al isabelle ]$ TPTP=/mnt/vault/TPTP-v6.4.0 isabelle tptp_translate FOF /mnt/vault/TPTP-v6.4.0/Problems/SET/SET002+3.p > /tmp/fof1

[al isabelle ]$ TPTP=/mnt/vault/TPTP-v6.4.0 isabelle tptp_isabelle 6000 /tmp/fof1
0:00:41 elapsed time
*** /tmp/fof1[1:4] syntax error: deleting UNSIGNED_INTEGER COLON UNSIGNED_INTEGER

*** At command "ML" (line 1 of "/tmp/Scratch_tptp_isabelle_1814_27692.thy")
Exception- TOPLEVEL_ERROR raised

view this post on Zulip Email Gateway (Aug 22 2022 at 15:13):

From: Nik Sultana via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Albert, in addition to Jasmin's helpful reply I thought to mention that you can find the TPTP-related code in the ${ISABELLE_HOME}/src/HOL/TPTP directory, as can be seen at:
http://isabelle.in.tum.de/repos/isabelle/file/a7394aa4d21c/src/HOL/TPTP
I'm not sure if you only intend to use this from the shell, but in case you're needing to write code then there's an example of using the TPTP-to-Isabelle interface from ML here:
http://isabelle.in.tum.de/repos/isabelle/file/a7394aa4d21c/src/HOL/TPTP/TPTP_Interpret_Test.thy

Turning to your email, this line suggests to me that your TPTP syntax might be malformed:
*** /tmp/fof1[1:4] syntax error: deleting UNSIGNED_INTEGER COLON UNSIGNED_INTEGER

From your output I gather that this file (/tmp/fof1) is generated by tptp_translate, which I don't know well enough to help you with. I also see that you start out by translating "/mnt/vault/TPTP-v6.4.0/Problems/SET/SET002+3.p" to produce "/tmp/fof1", and wonder if you've already tried to apply tptp_isabelle on SET002+3.p directly, without first running tptp_translate on it?

Best wishes,
Nik

view this post on Zulip Email Gateway (Aug 22 2022 at 15:13):

From: Albert Berger <nbdspcl@gmail.com>
On Wed, Mar 08, 2017 at 09:42:48PM +0000, Nik Sultana wrote:

Hi Albert, in addition to Jasmin's helpful reply I thought to mention that you can find the TPTP-related code in the ${ISABELLE_HOME}/src/HOL/TPTP directory, as can be seen at:
http://isabelle.in.tum.de/repos/isabelle/file/a7394aa4d21c/src/HOL/TPTP
I'm not sure if you only intend to use this from the shell, but in case you're needing to write code then there's an example of using the TPTP-to-Isabelle interface from ML here:
http://isabelle.in.tum.de/repos/isabelle/file/a7394aa4d21c/src/HOL/TPTP/TPTP_Interpret_Test.thy

Turning to your email, this line suggests to me that your TPTP syntax might be malformed:
*** /tmp/fof1[1:4] syntax error: deleting UNSIGNED_INTEGER COLON UNSIGNED_INTEGER

From your output I gather that this file (/tmp/fof1) is generated by tptp_translate, which I don't know well enough to help you with. I also see that you start out by translating "/mnt/vault/TPTP-v6.4.0/Problems/SET/SET002+3.p" to produce "/tmp/fof1", and wonder if you've already tried to apply tptp_isabelle on SET002+3.p directly, without first running tptp_translate on it?

Best wishes,
Nik

Many thanks, Nik! The example in the TPTP directory is very useful.

As for the syntax error, it turned out, that the translating script
prints to stdout not only the translated code, but also various status
messages, which were written into the translated file. After deleting
those messages from the file, all works OK.

Best regards.

Albert Berger.

On Wed, 8/3/17, Albert Berger <nbdspcl@gmail.com> wrote:

Subject: [isabelle] The correct way of using TPTP files with Isabelle?
To: cl-isabelle-users@lists.cam.ac.uk
Date: Wednesday, 8 March, 2017, 14:42

Greetings!

I'm trying to understand how to use Isabelle for proving
theorems from TPTP
collection. And I haven't succeed in that.

When I call 'isabelle tptp_isabelle' with a TPTP ".p" file
as an argument, I keep
getting all failures as the result. I tried 50, 600, and
6000 timeouts and the
most simple theorems.

When I first translate a TPTP file with 'isabelle
tptp_translate' and after that
call 'tptp_isabelle' with the translated file, I am getting
a "syntax error".

Could someone please advise the correct way of using
Isabelle for solving TPTP
theorems?

Thanks.

Albert Berger.

P.S. Below are two examples of shell output for both cases.

[al isabelle ]$ TPTP=/mnt/vault/TPTP-v6.4.0 isabelle
tptp_isabelle 6000
/mnt/vault/TPTP-v6.4.0/Problems/NUM/NUM005-1.p
0:00:33 elapsed time
running nitpick for 150 s
FAILURE: nitpick
running simp for 300 s
FAILURE: simp
running blast for 300 s
FAILURE: blast
running auto+spass for 600 s
FAILURE: auto+spass
running fast for 300 s
FAILURE: fast
running z3 for 150 s
FAILURE: z3
running cvc4 for 150 s
FAILURE: cvc4
running best for 150 s
FAILURE: best
running force for 300 s
FAILURE: force
running meson for 300 s
FAILURE: meson
running fastforce for 300 s
FAILURE: fastforce
running spass for 500 s
FAILURE: spass
running vampire for 500 s
FAILURE: vampire
running e for 500 s
FAILURE: e
running z3_tptp for 500 s
FAILURE: z3_tptp
running spass(1) for 250 s
FAILURE: spass(1)
running e(2) for 250 s
FAILURE: e(2)
running vampire(1) for 250 s
FAILURE: vampire(1)
running vampire(2) for 250 s
FAILURE: vampire(2)
running vampire(*) for 6000 s
FAILURE: vampire(*)
% SZS status GaveUp
poly: : warning: The type of (it) contains a free type
variable. Setting it to a unique

[al isabelle ]$ TPTP=/mnt/vault/TPTP-v6.4.0 isabelle
tptp_translate FOF
/mnt/vault/TPTP-v6.4.0/Problems/SET/SET002+3.p >
/tmp/fof1

[al isabelle ]$ TPTP=/mnt/vault/TPTP-v6.4.0 isabelle
tptp_isabelle 6000 /tmp/fof1
0:00:41 elapsed time
*** /tmp/fof1[1:4] syntax error: deleting 
UNSIGNED_INTEGER COLON UNSIGNED_INTEGER

*** At command "ML" (line 1 of
"/tmp/Scratch_tptp_isabelle_1814_27692.thy")
Exception- TOPLEVEL_ERROR raised

view this post on Zulip Email Gateway (Aug 22 2022 at 15:14):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Albert,

I'm trying to understand how to use Isabelle for proving theorems from TPTP
collection. And I haven't succeed in that.

When I call 'isabelle tptp_isabelle' with a TPTP ".p" file as an argument, I keep
getting all failures as the result. I tried 50, 600, and 6000 timeouts and the
most simple theorems.

The NUM005-1.p problem has a rating of 1.0. This means that no state-of-the-art provers can solve it, i.e. it is very difficult. If you try SET002+3.p instead, you should see

running nitpick for 150 s
FAILURE: nitpick
running simp for 300 s
SUCCESS: simp
% SZS status Theorem

i.e. you've just proved a theorem.

When I first translate a TPTP file with 'isabelle tptp_translate' and after that
call 'tptp_isabelle' with the translated file, I am getting a "syntax error".

I tried exactly what you did and I get the same output as above (i.e. theorem). I'm attaching the generated "fof1" file. Without more details, I'm afraid I don't know what's going on on your side.

Cheers,

Jasmin
fof1

Last updated: Apr 19 2024 at 01:05 UTC