This package redistributes material from the TPTP World, which is not covered by
the MIT licence in LICENSE.
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.
-- https://tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=ReadMe
The redistributed file, attributed to the TPTP and carried unmodified:
priv/bnf/SyntaxBNF-v9.3.1.3
The TPTP syntax BNF, version 9.3.1.3, taken as plain text from
https://tptp.org/UserDocs/TPTPLanguage/SyntaxBNF.html
sha256 17970a57e950d8dd768c2c691f0f493dd98d623669c5a39ca17c7e12993086d6
It is vendored so that installing this package needs no network access, and is the
text content of its page character for character, with no trailing newline. Nothing
in this repository edits it. The files under lib/ and src/ that are derived from it
are produced by `mix tptp.gen` and are regenerated rather than hand-maintained.
A second piece of TPTP material is carried without being redistributed as a file.
lib/tptp/szs/ontology.ex transcribes the SZS ontology published at
https://szs.tptp.org: the 112 value names, their mnemonics, their ontology and
subontology, and the description of each, the last of these quoted from the page
in the TPTP's own words. The transcription is maintained by hand and was last
checked against the page on 2026-09-10. It is offered as attributed verbatim
quotation of the published text; no wording is altered.
The SZS ontology moved to https://szs.tptp.org during 2026; the former address,
https://tptp.org/UserDocs/SZSOntology, now serves a notice pointing there.
Note that the BNF served by SeeTPTP under Category=Documents lags the UserDocs page:
at the time of writing it is version 9.3.0.4. The UserDocs page above is the source
to check against, not that one.
TPTP World is the work of Geoff Sutcliffe. See https://tptp.org.