Unquoted predicate names in TPTP output
TpmKranz opened this issue · 2 comments
Predicate names that should be quoted because they contain non-alphanumeric symbols are output verbatim, thus breaking parsing.
Example TPTP output:
ga_left_unit_max.txt
pNat*Nat___<=__ is the big offender here.
Input TIP problem, if of interest:
mytotalnumbers_Nat__E1_ga_left_unit_max1315634022635723058.txt
Command line:
zipperposition --input=tip --output=tptp --mode=fo-complete-basic --induction mytotalnumbers_Nat__E1_ga_left_unit_max1315634022635723058.txt
It's been a while, do you know what the escaping rules for TPTP are? Anything not in [A-Za-z0-9]+ (with underscores perhaps)?
If I interpret the syntax correctly, predicate names should just be atomic_words, which must be escaped if not matching [a-z][A-Za-z0-9_]*. I'm not sure that #94 is the right approach for that since it only seems to check for very specific cases outside that regex. Is regex matching not an option?
Sorry that I'm not familiar enough with OCaml to whip up a PR myself.