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
Email Gateway (Apr 10 2026 at 08:41):From: Jiangjing Xu <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle Developers,
I would like to follow up on the previously discussed TPTP keyword collision
issue in Sledgehammer.
Update on Zipperposition:
The parser issue in Zipperposition that caused parse errors when user-defined
symbols coincided with TPTP statement-level keywords (fof, tff, cnf, thf,
include) has been fixed in Parse_tptp.mly. Minimal reproductions now parse
correctly, and standard TPTP declarations continue to work as expected. PR
#103 implements this fix.
Defensive suggestion for Sledgehammer:
Although the Zipperposition parser fix resolves the immediate parse failures,
other ATP systems with strict parsers could theoretically be affected.
Currently, in src/HOL/Tools/ATP/atp_problem.ML, the avoid_clash function for
TPTP format is the identity function I.
As a precautionary measure, one could introduce an
avoid_clash_with_tptp_keywords function, analogous to the DFG version
(avoid_clash_with_dfg_keywords), that renames symbols colliding with the five
TPTP keywords (fof, tff, cnf, thf, include) and wire it into the TPTP branch
of avoid_clash. This modification is safe for readability, since only these
five keywords are renamed.
Illustrative modification:
(* Add this function for TPTP keyword avoidance *)
fun avoid_clash_with_tptp_keywords s =
if List.exists (fn kw => kw = s) ["fof", "tff", "cnf", "thf", "include"]
then
s ^ "_"
else
s
(* Apply to all non-DFG formats *)
val avoid_clash =
(case format of
DFG _ => avoid_clash_with_dfg_keywords
| _ => avoid_clash_with_tptp_keywords)
This ensures all formats that output TPTP syntax (FOF, TFF, THF, CNF, CNF_UEQ)
are protected, preventing parser-specific conflicts while leaving other
symbols unchanged.
Thank you for considering this suggestion.
Best regards,
Jiangjing Xu
Last updated: Apr 12 2026 at 02:50 UTC