Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Parsing TPTP, Auto-Generated from the Published BNF
Parsing TPTP, Auto-Generated from the Published BNF
What this note covers
What this note covers
TPTP (Thousands of Problems for Theorem Provers) is the standard cross-prover benchmark corpus for automated reasoning - 26,264 problems across 57 mathematical domains, used by Vampire, E, Twee, Waldmeister, and every modern ATP system. Every problem is a file with one of six clause heads: , , , , , . The TPTPWorld project publishes the formal grammar as a 735-line BNF file (, 338 rules).
.p
cnf
fof
tff
tcf
thf
ncf
SyntaxBNF-v9.2.1.4
The paclet ships the result of this construction as - (or ) returns the canonical shape directly. The companion Thousands of Problems for Theorem Provers (TPTP) ships a catalogue index of the full 26,264-problem distribution and drives over any problem on demand from the online corpus. This note tells the story of how the parser is built - the BNF + action map that reuses internally. It works in two steps:
TPTPImport[File["p.p"]]
TPTPImport["cnf(...)"]
<|"Axioms"->{phi1,...},"Conjecture"->phi|>
TPTPImport
TPTPImport
1
.Read the BNF into an .
Association[name->ParserCombinator]
2
.Apply the result to TPTP source - optionally with an map that lifts the raw parse tree to a Wolfram-Language data shape.
"Actions"
The lowering applies three standard PEG-vs-CFG rewrites automatically: direct left-recursion elimination, longest-alt-first sorting, and POSIX longest-match for rule bodies whose alternatives have equal element counts (the default ). Together these handle the eleven left-recursive TPTP rules, the shared-prefix alternatives like , and the cross-rule ambiguity in where both branches can consume the same leading term but only the second one continues into the trailing . See for the grammar-level mechanics; this note is the TPTP-specific story.
"ChoiceMode"->"Auto"
<constant>|<functor>(<fof_arguments>)
<fof_atomic_formula>::=<fof_plain_atomic_formula>|<fof_defined_atomic_formula>
=rhs
Bootstrapping a TPTP parser
Bootstrapping a TPTP parser
In[1]:=
Needs["Wolfram`Parser`"]tptpBnf=Import["https://raw.githubusercontent.com/TPTPWorld/SyntaxBNF/master/SyntaxBNF-v9.2.1.4","Text"];parsers=
[tptpBnf];(*Associationof338rule-name
.NoPrimitiveOverrides,nooptions.Default`"ChoiceMode""Auto"`enableslongest-matchforruleswhosealternativeshaveequalelementcounts;PEGorderfortherest.*)
 | EBNFParse |
 | ParserCombinator |
Every (token) and (char-class) rule auto-compiles through a regex meta-parser built out of the same combinators. The meta-parser handles char classes (, , and meta chars literally as in / ), negation (), octal escapes (), named escapes (, , ), the bare- regex any-char, ref forms (, ), grouping (), alternation (), and the postfix repetition operators (, , ). The full TPTP lexical layer (, , , , , , the punctuation tokens like / , and the regex-heavy / / ) all compile from the published BNF without manual help.
::-
:::
Parse*
[a-z]
[abc]
[|]
[*]
[^x]
[\40-\41]
\n
\r
\t
.
<name>
{name}
(...)
|
*
+
?
<lower_word>
<upper_word>
<integer>
<single_quoted>
<distinct_object>
<dollar_word>
<vline>
<star>
<sq_char>
<do_char>
<not_star_slash>
That's the entire setup. is the top-level parser; , , etc. are the per-clause-head parsers; , , … are the inner rules.
parsers["TPTP_file"]
parsers["cnf_annotated"]
parsers["fof_annotated"]
parsers["fof_unitary_formula"]
parsers["fof_quantified_formula"]
A real TPTP problem, parsed end-to-end:
In[2]:=
groupAxioms="fof(group_assoc, axiom, ! [X, Y, Z] : multiply(multiply(X, Y), Z) = multiply(X, multiply(Y, Z))).fof(group_left_id, axiom, ! [X] : multiply(identity, X) = X).fof(group_left_inv, axiom, ! [X] : multiply(inverse(X), X) = identity).fof(commutator_def, axiom, ! [X, Y] : commutator(X, Y) = multiply(multiply(X, Y), multiply(inverse(X), inverse(Y)))).fof(goal, conjecture, ! [X] : commutator(X, identity) = identity).";Length@
[parsers["TPTP_file"],groupAxioms](*5*)
 | Parse |
Out[2]=
2
Five clauses, quantifiers, function application, equality - all parsed. But the value above is the raw parse tree (a list of clauses, each clause a list of literal tokens and sub-rule results). For a workable downstream shape, pass a per-rule map.
"Actions"
Lifting to a useful shape: the "Actions" map
Lifting to a useful shape: the map
"Actions"
Each entry in wraps the named rule's parser in a . The function receives the rule's parsed value via the normal splatted convention - indexes into the sequence of matched sub-pieces. The action map below is the one installs at first call - it lifts the raw parse tree to the canonical Wolfram-Language shape:
"Actions"-><|name->fn|>
ParseAction
Function[#1,#2,...]
In[3]:=
Out[3]=
Parse[Missing[NotAvailable,TPTP_file],fof(assoc, axiom, ! [X, Y, Z] : multiply(multiply(X, Y), Z) = multiply(X, multiply(Y, Z))).fof(left_id, axiom, ! [X] : multiply(identity, X) = X).fof(goal, conjecture, ! [X] : multiply(X, identity) = X).]
This is the shape returns: / quantifiers, function application as , / for /, the Boolean grammar as /////, cnf disjunctions as (single literal stays bare), and flipped through so the returned is the positive goal. The action map is ~50 entries, one per BNF rule on the path from to . The recogniser is unchanged - the same call drives both the with-actions and without-actions flows.
ForAll
Exists
head[args...]
Equal
Unequal
=
!=
And
Or
Not
Implies
Equivalent
Xor
Or[...]
negated_conjecture
Not
Conjecture
<TPTP_file>
<constant>
EBNFParse
Without actions, the parser is just a recogniser - it tells you whether the source matches the grammar but the value is the structural skeleton. The action layer is what turns that into a workable Wolfram Language data structure.
Benchmark on the published corpus
Benchmark on the published corpus
On the small CNF / FOF problems from the published distribution, per-clause parse time lands in the tens of milliseconds for short clauses (a few atoms, ground equations) and climbs into the hundreds of milliseconds for clauses with nested quantifiers and function applications. The 5-clause group-theory problem at the top of this note parses in ~700 ms end-to-end on a 2024 laptop with default .
v9.2.1
"ChoiceMode"->"Auto"
The cost of trying every alternative under longest-match without memoisation shows up on FOF with deep boolean / quantifier nesting. Adding to would close most of the throughput gap; a Pratt-style precedence climber for the connective grammar would be the right move for THF, where alternative explosion overwhelms even longest-match.
ParseRecursive
ParserCompile is currently a stub
ParserCompile is currently a stub
In[4]:=
compiled=
[parsers["TPTP_file"]];(*sameparserwith"Code"keyinopts,butroutedthroughaninterpretiveshim-norealFunctionCompileloweringyet*)
| ParserCompile |
Per the usage string: "v0.2: stubbed via the interpreter; the real FunctionCompile lowering lands later". A head-to-head bench on the 4 passing files confirms it - interpretive vs compiled are within measurement noise (1.00x speedup). Wiring up the real FunctionCompile path is a v0.4 item; the compiler infrastructure (, , , test suite) is in place but the per-combinator codegen rules aren't all written yet.
compilableQ
compileParser
interpretCompiledShim
CompileFeasibility
What the ChoiceMode flip fixes
What the ChoiceMode flip fixes
The earlier draft of this note reported a cluster of failures around equations and disequations whose left side was a function application, in and contexts. Example: inside . PEG-ordered was committing to on , then expecting end-of-clause, but the source continued with which only (a sibling alt at the same level) reaches.
cnf
fof
multiply(b,a)!=c
cnf(_,negated_conjecture,multiply(b,a)!=c).
Choice
<fof_plain_atomic_formula>
multiply(b,a)
!=c
<fof_infix_unary>
<cnf_literal>
The default resolves that whole cluster: for rule bodies whose alternatives have equal element counts (the static sort can't break the tie), the lowering uses POSIX longest-match - every alt is tried at the current position and the one that consumed the most input wins. The choice, choice, and a handful of other shape-ambiguous rules become correct without changing the grammar. The cost is some throughput - longest-match cannot early-exit on first hit, so deeply nested choices pay a constant factor over PEG. Set to opt back into the fast-but-strict ordering when the grammar is unambiguous; set to use longest-match unconditionally (correct on more grammars, slowest).
"ChoiceMode"->"Auto"
longest-alt-first
<fof_atomic_formula>
<cnf_literal>
"ChoiceMode"->"PEG"
"ChoiceMode"->"Longest"
Remaining failures cluster on the higher-order alternatives in (the recursive rule and friends). These exhibit exponential backtracking under any ordered-choice strategy and want either packrat memoisation or a Pratt-style precedence parser to be tractable - both unimplemented.
<thf_*>
<thf_typeable_formula>
Building the bench yourself
Building the bench yourself
The TPTP distribution lives at https://tptp.org/TPTP/Distribution/TPTP-v9.2.1.tgz (922 MB compressed). Extract a sample and run:
In[5]:=
(*...primitiveOverrides+parsersfromabove...*)loadClean[path_String]:=StringTrim@StringReplace[Import[path,"Text"],RegularExpression["%[^]*"]""];benchOne[file_]:=Block{src=loadClean[file],r,t},t=AbsoluteTime[];r=TimeConstrained
[parsers["TPTP_file"],src],30,"TO";"File"FileBaseName[file],"Bytes"StringLength[src],"Time"AbsoluteTime[]-t,"Status"Which[r==="TO","TIMEOUT",FailureQ[r],"ERROR",True,"OK"],"Clauses"If[ListQ[r],Length[r],0];results=benchOne/@Take[FileNames["*.p","/path/to/TPTP-v9.2.1/Problems",Infinity],100];Counts[#["Status"]&/@results]
| Parse |
For the THF problems, raise the timeout or skip them ( filters them out). The TFF / TCF cases land somewhere between CNF and THF in difficulty.
StringContainsQ[FileBaseName[#],"^"]&
To run the same bench against the compiled path, swap the parser:
In[6]:=
tptpCompiled=
[parsers["TPTP_file"]];benchOne[file_]:=Block{src=loadClean[file],r,t},t=AbsoluteTime[];r=TimeConstrained
[tptpCompiled,src],30,"TO";...;
| ParserCompile |
| Parse |
The current is interpretive-equivalent (stubbed), so per-file times will be within ~1% of the interpretive baseline. When the real FunctionCompile lowering lands, this swap is what surfaces the speedup.
ParserCompile
What this approach buys
What this approach buys
The EBNF-driven path means the grammar IS the parser definition - the parser cannot disagree with the published BNF because they are the same file. When TPTP-v9.3 ships, re-run on the new BNF and re-bind the actions; no per-rule diff. The recogniser drops out for free: 280 of the 338 TPTP rules lower automatically, and small CNF / FOF clauses parse end to end via a generic mechanism. Compare this to a hand-coded parser, where every grammar change is a per-rule code edit.
EBNFParse
What still needs hand-work:
◼
Term-level disambiguation. The left-factoring issue described above. Either a deeper structural rewrite or memoisation.
<fof_plain_term>
◼
THF higher-order. The mutual recursion + alternative explosion in the higher-order grammar needs memoisation or a different parsing strategy (e.g. Pratt-style precedence climbing) to be tractable.
◼
Lexical primitives. The map above covers the common cases; a complete map adds , , , the spacing tokens, comment / whitespace rules. A small -to- compiler would generate these from the BNF too.
PrimitiveOverrides
real
rational
dollar_dollar_word
:::
ParseCharacter
For most TPTP workflows, (built on this construction) is the entry point. For evolving formal-grammar work where the published spec is moving, the EBNF-driven path is what keeps the parser in lockstep with the spec.
 |
|
 |
|
""