Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unquoted predicate names in TPTP output #93

Open
TpmKranz opened this issue Oct 16, 2022 · 2 comments
Open

Unquoted predicate names in TPTP output #93

TpmKranz opened this issue Oct 16, 2022 · 2 comments

Comments

@TpmKranz
Copy link
Contributor

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

@c-cube
Copy link
Member

c-cube commented Oct 17, 2022

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)?

@TpmKranz
Copy link
Contributor Author

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.

abentkamp added a commit that referenced this issue Oct 31, 2022
try to fix escaping of identifiers in TPTP output (#93)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants