Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Running Isabelle/Sledgehammer with TPTP input

view this post on Zulip Email Gateway (Aug 23 2022 at 09:18):

From: Julien Narboux <narboux@unistra.fr>
Hi,

I am trying to test Isabelle /Sledgehammer on some examples expressed using the TPTP syntax for FOF.

On linux using Isabelle2016:

Isabelle2016/bin/isabelle tptp_isabelle 300 foo.p
Works and returns sometimes: SZS Status Theorem

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.

What is the correct command for recent Isabelle versions ?

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 ?

Is there a way to activate output of the readable proof in Isar format from the command line ?

I have seen another script called tptp_sledgehammer, what is the difference ?

Regards,

Julien Narboux

Last updated: Apr 25 2024 at 08:20 UTC