Re: [isabelle] The correct way of using TPTP files with Isabelle?



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

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

 Subject: [isabelle] The correct way of using TPTP files with Isabelle?
 To: cl-isabelle-users at 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
 
 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.