Email Gateway (Mar 17 2026 at 12:01): Email Gateway (Mar 17 2026 at 12:01):From: Jiangjing Xu <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
I would like to report what appears to be a bug in Sledgehammer's TPTP export. This may be related to the recently discussed Sledgehammer/ATP name-clash issues, but the failure mode here seems slightly different: the generated identifier appears to collide with TPTP surface syntax rather than merely with another generated name.
If a free variable in an Isabelle goal has the same name as a TPTP statement-level keyword such as fof, tff, cnf, thf, tcf, or include, Sledgehammer appears to export it unchanged as a symbol name in the generated TPTP problem file. This appears to produce declarations that Zipperposition cannot parse.
Minimal example:
theory Test
imports Main
begin
lemma "fof = (fof :: nat)"
sledgehammer [prover = zipperposition, slices = 1, timeout = 30, overlord]
oops
end
The generated problem file (retained via overlord) contains:
thf(sy_v_fof, type,
fof : nat).
Zipperposition reports:
parse error: expected declaration
at file '.../prob_zipperposition_1.p'
I have observed the same pattern for other names such as tff, cnf, thf, tcf, and include, where the generated TPTP output contains bare statement-level keywords as symbol names. In my tests, these variants likewise lead to ATP-side parse failures.
By contrast, identifiers such as type or axiom, which are TPTP role values rather than statement-level introducers, do not seem to trigger this problem, and Sledgehammer works as expected there.
My understanding is that Sledgehammer's nice-name mapping should avoid producing bare TPTP statement-level keywords as exported symbol names.
Environment:
* Isabelle 2025-2
* Zipperposition
* macOS (arm64)
I can provide the full generated .p files and additional reproducing examples if useful.
Best regards,
Jiangjing Xu
Email Gateway (Mar 18 2026 at 19:38):From: Alexander Steen <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
this looks like a Zipperposition parser bug, not a Sledgehammer bug.
TPTP does not prohibit the use of "fof" as symbol name, and other ATP
systems do not complain about it.
Best, Alex
On 3/17/26 12:59, Jiangjing Xu (via cl-isabelle-users Mailing List) wrote:
Dear Isabelle developers,
I would like to report what appears to be a bug in Sledgehammer's TPTP
export. This may be related to the recently discussed Sledgehammer/ATP
name-clash issues, but the failure mode here seems slightly different:
the generated identifier appears to collide with TPTP surface syntax
rather than merely with another generated name.If a free variable in an Isabelle goal has the same name as a TPTP
statement-level keyword such as |fof|, |tff|, |cnf|, |thf|, |tcf|, or
|include|, Sledgehammer appears to export it unchanged as a symbol
name in the generated TPTP problem file. This appears to produce
declarations that Zipperposition cannot parse.Minimal example:
|theory Test imports Main begin lemma "fof = (fof :: nat)"
sledgehammer [prover = zipperposition, slices = 1, timeout = 30,
overlord] oops end |The generated problem file (retained via |overlord|) contains:
|thf(sy_v_fof, type, fof : nat). |
Zipperposition reports:
|parse error: expected declaration at file
'.../prob_zipperposition_1.p' |I have observed the same pattern for other names such as |tff|, |cnf|,
|thf|, |tcf|, and |include|, where the generated TPTP output contains
bare statement-level keywords as symbol names. In my tests, these
variants likewise lead to ATP-side parse failures.By contrast, identifiers such as |type| or |axiom|, which are TPTP
role values rather than statement-level introducers, do not seem to
trigger this problem, and Sledgehammer works as expected there.My understanding is that Sledgehammer's nice-name mapping should avoid
producing bare TPTP statement-level keywords as exported symbol names.Environment:
*
Isabelle 2025-2
*
Zipperposition
*
macOS (arm64)
I can provide the full generated |.p| files and additional reproducing
examples if useful.Best regards,
Jiangjing Xu--
Prof. Dr. Alexander Steen
Universität Greifswald
Institut für Mathematik und Informatik
Walther-Rathenau-Straße 47
17489 Greifswald
Tel.: +49 3834 420 4634
Tel.: +49 3834 420 4614 (secretary)
E-Mail:alexander.steen@uni-greifswald.de
Zoom:https://uni-greifswald-de.zoom.us/my/a.steen
Email Gateway (Mar 18 2026 at 20:36):From: Jiangjing Xu <cl-isabelle-users@lists.cam.ac.uk>
Dear Prof. Dr. Alexander Steen,
Thank you for pointing this out. I have since tested the same format with
Vampire and Z3, and both accept it without error, which confirms your
assessment that the TPTP output is valid and the issue is on the
Zipperposition parser side.
Thank you again for the clarification.
Best regards,
Jiangjing Xu
Last updated: Mar 21 2026 at 20:30 UTC