Tptp.Statement.Annotated (Tptp v0.1.0)

Copy Markdown View Source

An annotated formula: fof(name, role, formula, source, info).

Retention of source and info

These fields constitute the TSTP. A derivation is a set of annotated formulae whose source records the inference producing each one and the parents it was derived from, so a reader discarding them can read problems but not proofs. They are already parsed, the grammar covering <source> and <useful_info> in full, so retaining them allows proof reconstruction to be a traversal rather than a second parse.

Uninterpreted fields

role is the node as parsed rather than an atom from a closed set: <formula_role> is a <lower_word> in the ::= grammar and is restricted to the named set only by the :== conditions, so rejecting an unrecognised role is a lint decision rather than a parse decision. Likewise formula is the unelaborated subtree; in a THF statement it may be a type, a term or a formula, and the grammar does not distinguish them.

Summary

Types

t()

One annotated formula, with its four grammatical slots kept apart as separate subtrees.

Types

t()

@type t() :: %Tptp.Statement.Annotated{
  formula: Tptp.Node.t(),
  info: Tptp.Node.t() | nil,
  language: :thf | :tff | :tcf | :fof | :cnf | :tpi,
  len: non_neg_integer(),
  name: Tptp.Node.t(),
  off: non_neg_integer(),
  role: Tptp.Node.t(),
  source: Tptp.Node.t() | nil
}

One annotated formula, with its four grammatical slots kept apart as separate subtrees.