tptp

A span-preserving parser, linter and printer for the TPTP language, generated from the published BNF.

No runtime dependencies. yecc and :crypto are supplied by OTP and the lexer is hand-written, so the package is straightforward to vendor.

def deps do
  [{:tptp, "~> 0.1"}]
end

Function

1. Scan TPTP source into tokens with byte-accurate spans.
2. Split the token stream into statements, bounding the effect of malformed input to a single statement.
3. Parse each statement into a concrete syntax tree whose node kinds are BNF nonterminals.
4. Resolve include directives against a pluggable resolver — the local filesystem under $TPTP_ROOT, or tptp.org over HTTPS — with cycle detection.
5. Check the :== well-formedness conditions and the cross-statement conditions.
6. Print a tree back to TPTP: canonical, pretty, or format-preserving.
7. Read the SZS status lines emitted by ATP systems, over the 112 values and the isa hierarchy of the published SZS ontology BNF.

Scope

The library performs no type checking, no normalisation and no elaboration, and attaches no semantics to the operators it recognises.

THF requires a declaration for every symbol and a type on every bound variable, and the first-order typed dialects fix a default for whatever they leave out — $i for an untyped variable, ($i * ... * $i) > $i or > $o for an undeclared function or predicate — so no type inference is required to read any of them, and none is performed. Explicit type arguments are recorded verbatim, in source order and with spans: in f @ $i @ a the $i is retained as an argument of the application.

It follows that the tree does not distinguish a THF type from a THF term. The grammar does not either: <thf_unitary_type> ::= <thf_unitary_formula> identifies the two nonterminals, and the :== conditions are what restrict a formula to those admissible as types. Elaboration against a signature belongs to the consumer.

Analysis

An editor integration requires the file, its diagnostics, the symbol table and the dialect on each edit. Tptp.analyze/2 produces all four as a Tptp.Analysis from a single traversal, Tptp.Lint.scan/2, of which Tptp.Lint.run/2, run_unit/2 and table/1 are projections.

Conversion of byte offsets to line and column is excluded from that traversal, since an analysis that is never rendered should not incur a scan of the source and one rendering many positions should incur it once. with_line_index/1 performs it.

Input that does not parse still yields an analysis carrying the diagnostics that record the failure, since an editor must render markers for a buffer it cannot parse.

Tptp.Analyzer is the underlying behaviour: a named producer of diagnostics over an analysis, declaring the dialects it applies to. Tptp.Lint implements it as :tptp_lint; a prover-backend probe or a project naming convention would be other implementations. Tptp.Analyzer.run_all/3 dispatches by dialect and distinguishes two outcomes that are easily conflated: an analyzer excluded by dialect reports :skipped rather than an empty list. An analyzer that raises is contained as a TPTP0800 diagnostic naming it.

Coverage

Every problem and axiom file of a complete TPTP v9.3.1, across all dialects, through the parser alone: no include resolved and no lint rule applied.

5.4 GB in 887 seconds on eight workers, under a 60-second per-file budget that no file reached. The preceding toolchain recorded 628 timeouts and 221 parse failures over the TH0/TH1 subset alone.

The four failures are SYN000-2.p, SYN000+2.p, SYN000_2.p and SYN000^2.p, the annotated-formula demonstration written once per dialect, and they are defects in the files rather than in the parser. Three use theory(equality) as an inference parent, which <source> has not derived since v9.3.1.2 replaced <source> ::= <general_term> with a list of alternatives; that was fixed upstream on 10/09/26 and the three parse once the edit reaches the distributed tarball. SYN000_2.p carries a second, independent one — it writes introduced(assumption,[from,the,world,[]]) where both the BNF and the language page state introduced(<intro_type>,<useful_info>,<parents>), the other three dialects' copies writing introduced(assumption,[from,the,world],[]). CORPUS.md carries the citation for each.

The TPTP is this library's ground truth: where the two disagree, the parser is incorrect, being generated from the published BNF, and correcting it by hand would make it a parser for something else. Where the published sources disagree with each other — the grammar rejecting a file the TPTP distributes, or one page contradicting another — the disagreement is reported upstream rather than worked around. Six such disagreements were carried here during development; BNF v9.3.1.3 and the SZS ontology's move to szs.tptp.org resolve all of them, and the register that held them is gone with them.

The 65 problems above 20 MB — 64 HWV and LCL680+1.020.p, 3.7 GB between them — are read by stream_file!/2 rather than by this sweep. The size limit is a property of the report rather than of the parser.

FINDINGS.md records what the four failures were hiding from the stages after the parser, and what a sweep of the library turned up once they were patched out of a copy: two further defects in those files, and three rules of this library's that were wrong.

mix tptp.corpus writes CORPUS.md, from which these figures are taken and which the nightly workflow regenerates. mix tptp.census writes CENSUS.md, recording where the library applies a type constructor and in which dialects — a question about the corpus rather than the parser, and one an elaborator built on this library must answer.

Generated sources

Five files are generated from the two vendored TPTP World BNFs and committed, so installation requires neither Python, nor awk, nor the BNFs, nor network access:

Regeneration is a maintainer action performed on a TPTP release, and the resulting diff constitutes the review of that release.

mix tptp.gen           # regenerate all five
mix tptp.gen --check   # fail if any committed output is stale

The generator reports its three departures from a mechanical translation, each of which would otherwise constitute an LALR(1) conflict. The list is produced by Tptp.Bnf.Generator.departures/0 from the constants causing it, so a release requiring a fourth is reported rather than absorbed silently.

Tptp.Szs.Ontology is generated from SZSOntology.bnf, the TPTP World's source of truth for the three SZS ontologies: the 112 values, the ontology each belongs to, and the isa hierarchy among them, which is a DAG rather than a tree (Theorem has three parents). parents/1, children/1, ancestors/1, descendants/1 and isa?/2 are read off the BNF's rules and nothing is transcribed from a diagram. The one thing the BNF does not carry — the mnemonics and descriptions of the values — Tptp.Szs.Page transcribes from the ontology page by hand, and a test fails the build when a value the BNF defines has no entry there.

The SyntaxBNF references <status_value> from <inference_status> and no longer defines it; the SZS BNF states the list as <inference_status_value>, and Tptp.Bnf.Vocabulary takes it from there under the name the reference uses. The generator refuses to run if the SyntaxBNF defines the rule again or stops referencing it.

Tptp.bnf_version/0 reports the TPTP BNF release the shipped parser was generated from. It is distinct from the package version, which is semantic versioning over the Elixir API.

Command line

Two of the library's functions are available without writing Elixir.

mix tptp.lint Problems/PUZ/PUZ001+1.p        # diagnostics as path:line:column
mix tptp.lint --include --severity warning "Problems/SYN/*.p"
mix tptp.lint --format json --only TPTP0501 problem.p
mix tptp.format --check "Axioms/**/*.ax"     # layout only; the tokens are unchanged

mix tptp.lint prints path:line:column: severity: message [CODE] and exits non-zero where any diagnostic at or above --severity was reported. --include resolves the include graph first, under which the undeclared-symbol rule and the conjecture count can be correct for a problem whose signature is supplied by an axiom set.

Example

examples/demo.livemd is a Livebook covering parsing, diagnostics, the three printers, includes, lint, SZS and the statement stream in approximately twenty cells. Open it in Livebook, or read it as Markdown.

Development

mix test               # unit and property tests
mix test --include corpus
mix test --include network   # re-checks the vendored files against their pages
mix check              # format, compile --warnings-as-errors, credo, test, dialyzer
mix run bench/parse.exs
mix tptp.corpus        # sweep a local TPTP library, rewrite reports/CORPUS.md
mix tptp.census        # the same library's type applications, rewrite reports/CENSUS.md

Both sweeps parse each file in a separate process under a max_heap_size ceiling, since a file's size does not predict the cost of parsing it: across the library the source ranges from 2.5 to 111 bytes per tree node, so SWV535-1.010.p peaks at 3.2 GB from 8 MB while a file twice its size peaks at a ninth of that. --heap is the total across all workers, and a parse exceeding its share is retried alone.

CI runs the stages of mix check as one job and Dialyzer as another, so the PLT is cached under its own key and a lock-file change does not rebuild it. A third workflow regenerates the generated files and fails if the working tree is not clean, which is what prevents a generated file from being hand-edited.

A fourth workflow reads the library. On a pull request it sweeps one file in five; nightly it sweeps every file, since a check skipping four files in five examines four fifths of nothing. Set $TPTP_CORPUS_FULL=1 to run the corpus tests that way locally.

Benchmarks

bench/parse.exs runs each stage over 1 KB, 100 KB, 1 MB and 4.5 MB inputs and reports allocation alongside throughput. The design of this library is largely a set of allocation decisions, and a timing alone would report a regression in any of them as acceptable until memory ran out.

The final rung is a bound rather than a measurement. Axioms/CSR002+5.ax is 455 MB, approximately 75 million tokens, which as three-tuples would occupy roughly 2.4 GB. It is streamed with the baseline taken after the source binary is read, so the figure reported is not the cost of the file, which is unavoidable, but whether the token stream was materialised alongside it.

On a Ryzen 7 3700X under OTP 28 and Elixir 1.20.3:

statements  3341977
elapsed     19.0 s
peak heap above the loaded file    238.1 KB

3.3 million statements from a 455 MB file, with a quarter of a megabyte of live heap above the source. The remaining rungs scale linearly: end to end, from_string runs at approximately 4 MB/s and allocates roughly 75 times the size of the source, that being the tree, which is why stream_string!/1 exists for larger input.

Lexer verification

The lexer is the only stage not derived from the BNF, so mix tptp.gen also writes test/support/bnf_oracle.ex: the 56 ::- and ::: rules transcribed into anchored regular expressions. The property asserted is not that the lexer matches the BNF but that every token the lexer emits without a diagnostic satisfies its BNF pattern, so a departure is admissible only where the lexer reports it. There are two, both warnings: an empty quoted token, which <single_quoted> and — since v9.3.1.3 — <distinct_object> both forbid, and a redundant leading zero, as in 00, -007 and 1/02.

Documentation and static analysis

Every module carries a @moduledoc, every public function a @doc and every type a @typedoc. test/tptp/documentation_test.exs enforces this from the compiled docs chunk rather than by review. Rationale a consumer requires belongs in the published documentation; the library is accordingly close to free of code comments, the exceptions being the sweep scheduler and the generators, where what requires explanation is the shape of an implementation rather than the behaviour of an API.

mix credo --strict includes a custom check prohibiting String.to_atom/1 and its equivalents. Atoms are never collected and the table is bounded at approximately one million, so a library reading tens of thousands of untrusted files must not create them from input. This is a security property and is enforced mechanically.

Licence

This library is MIT licensed. See LICENSE.

Redistributed TPTP material is not. priv/bnf/SyntaxBNF-v9.3.1.3 is the file from github.com/TPTPWorld/SyntaxBNF, priv/bnf/SZSOntology.bnf the file from github.com/TPTPWorld/SZSOntologies (CC BY 4.0), each carried unmodified so that installation requires no network access, and lib/tptp/szs/page.ex quotes the value descriptions from the SZS ontology page. The TPTP's terms permit this:

The TPTP is copyrighted 1993-onwards, by Geoff Sutcliffe & Christian Suttner. Verbatim redistribution of the TPTP and parts of the TPTP is permitted provided that the redistribution is clearly attributed to the TPTP. Distribution of any modified version or modified part of the TPTP requires permission.

None is modified. See NOTICE for the attribution, the commit each file was taken at and its digest, and tptp.org for the TPTP itself.