Email Gateway (Aug 23 2022 at 09:18): Email Gateway (Aug 23 2022 at 09:18):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Julien,
Using Isabelle2018 or Isabelle2020, the same command just list the signature of some ml files ending with « structure ATP_Problem_Import: ATP_PROBLEM_IMPORT, but the provers do not seem to be run and I always get a SZS Status GaveUp.
Looks like bit rot.
When the successful prover is not an Isabelle tactic, like vampire or spass, does that mean that the proof has been reconstructed successfully ? or the provers are considered as oracles ?
They're considered oracles. This could be changed easy.
Is there a way to activate output of the readable proof in Isar format from the command line ?
No. The goal of this setup, as you can guess, was to participate in the CASC competition. But since 2015 or 2016, CASC requires proof output in TSTP format (as opposed to just the status "theorem" or not), and I've never bothered trying to have Isabelle output proofs for CASC. Instead, I worked on a HO ATP, an effort that paid off at the latest CASC:
http://www.tptp.org/CASC/J10/WWWFiles/DivisionSummary1.html <http://www.tptp.org/CASC/J10/WWWFiles/DivisionSummary1.html>
(First row, "Zipperpin" = "Zipperposition").
I have seen another script called tptp_sledgehammer, what is the difference ?
Sledgehammer only calls Sledgehammer. Isabelle also calls "auto", "blast", etc.
These tools are very crude. I'll look into the bit rot issue and come back to you, but for the rest I'm afraid you're on your own. I'd gladly accept and apply patches though and can explain the code (there isn't much).
Cheers,
Jasmin
Email Gateway (Aug 23 2022 at 09:19):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Julien,
I have now fixed this in the development version of Isabelle. The trick is to remove the two invocations of the function "freeze_problem_consts", which were an unnecessary hack that had a minor impact on the success rate but that no longer works after some reforms in local theories. You can try to amend the file locally or wait for the next version.
Thank you for your report.
Cheers,
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC