v0.3.0

Added

• Tptp.Header, a public reader for the % Key : value header of a problem, an
  axiom set or a TSTP solution: from_string/2, from_file/2, get/2,
  entries/2 (a % : line starts a further entry, as in Refs),
  to_map/1, status/1 (Status, or a solution's Result, through the SZS
  ontology) and spc/1 (FOF_THM_RFO_SEQ as form, status and features).
• TPTP0901, a header line with no : after its key, in a new TPTP09xx tier.
  MGT087+1.p, MGT088+1.p, MGT105+1.p and MGT108+1.p of TPTP v9.3.1 write
  Refs, Source and Names that way; the reader had dropped those lines without
  a word.

Changed

• The parser is regenerated from TPTP BNF v9.3.1.6, which Tptp.bnf_version/0 now
  reports; it was v9.3.1.3. This breaks callers that name what it removed:

  • <comment_line> (::-) changed
  • <fof_binary_assoc> (::=) is no longer defined
  • <fof_binary_formula> (::=) no longer admits <fof_binary_assoc>
  • <fof_binary_formula> (::=) no longer admits <fof_binary_nonassoc>
  • <fof_binary_nonassoc> (::=) is no longer defined
  • <ntf_logic_name> (:==) no longer admits $temporal_instant
  • <printable_char> (:::) is no longer defined
  • <tff_binary_assoc> (::=) is no longer defined
  • <tff_binary_formula> (::=) no longer admits <tff_binary_assoc>
  • <tff_binary_formula> (::=) no longer admits <tff_binary_nonassoc>
  • <tff_binary_nonassoc> (::=) is no longer defined
  • <thf_binary_assoc> (::=) is no longer defined
  • <thf_binary_formula> (::=) no longer admits <thf_binary_assoc>
  • <thf_binary_formula> (::=) no longer admits <thf_binary_nonassoc>
  • <thf_binary_nonassoc> (::=) is no longer defined
  • <viewable_char> (:::) is no longer defined

  The BNF records what changed:

  % v9.3.1.4 - Changed <*_binary_assoc> to <*_binary_list> and <*_binary_nonassoc> to
  %            <*_binary_pair>, to reflect the intended non-associativity.
  % v9.3.1.5 - Changed <printable_char> ::: . to <comment_char> ::: [^\r\n], and replaced
  %            <printable_char> with <comment_char> in all uses. Removed unused <viewable_char>.
  %            Thanks to Jiazhen Xia for these fixes.
  % v9.3.1.6 - Removed $temporal_instant and added $intuitionistic as a <ntf_logic_name>
  

• The nodes of a binary formula with a non-associative connective are now of kind
  :fof_binary_pair, :tff_binary_pair and :thf_binary_pair, where they were
  :fof_binary_nonassoc, :tff_binary_nonassoc and :thf_binary_nonassoc. The
  children and the printed text are unchanged; <*_binary_list>, like
  <*_binary_assoc> before it, passes its child through and has no node.

• $intuitionistic is an <ntf_logic_name> and $temporal_instant is not, so
  Tptp.Bnf.Vocabulary.ntf_logic_name?/1 and reserved_word?/1 answer accordingly.

• Tptp.Tstp reads its header through Tptp.Header. A % : text line
  now contributes text to the value rather than : text, and from_string/2
  returns TPTP0901 among its diagnostics.

Removed

• verify/, the Lean 4 project, and the proofs workflow that built it. Its
  models were transcriptions of the Elixir by hand, so nothing kept them in step
  with the code they described; the oracle and property tests remain.

v0.2.1

Release 0.2.1

The file-source parent fix (061299e) landed after 0.2.0 was published,
so its CHANGELOG entry moves from 0.2.0 to a 0.2.1 section. The version
moves in mix.exs, CITATION.cff and .zenodo.json, the comparison links
gain 0.2.0 and 0.2.1, and the README's dependency line asks for ~> 0.2.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

v0.2.0

Release 0.2.0

Version, the `[0.2.0]` CHANGELOG section, and a `TSTP` docs group for the
five modules added: `Tptp.Derivation` with its node and step structs,
and `Tptp.Tstp` with its solution struct.

The README gains a "Derivations and TSTP files" section with one example
of each, and the Function list an eighth entry: reading a derivation is
a thing the library does now, not a note under the SZS reader.

The citation metadata says so too — a release that adds a reader for a
format is one someone may cite for that reader.

`Tptp.bnf_version/0` does not move: the grammar was not regenerated.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

v0.1.3

make parsing of status lines more loose

v0.1.2

Citation metadata (CITATION.cff, .zenodo.json) for archiving on Zenodo; no functional changes.

v0.1.1

Citation metadata (CITATION.cff, .zenodo.json) for archiving on Zenodo; no functional changes.

v0.1.0

Fix tptp corpus url in corpus.yml