Constructs the symbol table and the dialect feature set during the traversal.

Not a rule. It is applied before the rules at every node and produces the data read afterwards by the Tptp.Lint.Rule.review/2 callbacks, which is what allows Tptp.Lint to require a single pass.

Declarations

A type-role statement whose formula is an atom typing, such as tff(f_decl, type, f: $i > $o). The subject is recorded as declared and the right-hand side of the colon is stored verbatim as the declared type. It is not interpreted.

Uses

A constant, functor, defined_functor or system_functor, or their nullary counterparts, occurring within a formula — not within a name, role, source or info field. Never a variable: in X @ a the head is bound by its quantifier rather than declared by a type statement.

The annotations contain atoms indistinguishable in form from symbols that are not symbols: file in a <source> is a keyword and status(thm) is a label. Counting them would report the TSTP vocabulary as undeclared.

An <ntf_index> is the second such position. In {$necessary(#agent)} the word agent labels a modality rather than denoting a constant of the problem's signature, and SYN000^7.p, the reference example for the syntax, declares no type for it. The subtree beneath an ntf_index is therefore claimed before the traversal reaches it, and none of it is counted.

Symbol identity

'p' and p denote one symbol, since the BNF defines a <single_quoted> as the enclosed atomic word without its quotes. Every key passed to Tptp.Lint.Table is therefore taken from Tptp.Node.value/1 rather than from text. Keying on the spelling separates tff(t, type, 'p': $i > $o). tff(a, axiom, p(x)). into two entries, producing a spurious undeclared-symbol finding and a missed duplicate name, and propagates the separation to anything built on Tptp.Query.symbols/1. The same applies to statement names and to the names an inference record supplies as parents, since <name> ::= <atomic_word> | <integer>.

Arity

Arity is the length of the application spine, recorded at the application node. f(a, b) is a fof_plain_term with a functor and an argument list, so the arity is the length of that list; f @ a @ b is a left-nested application spine, so the arity is its depth. Both are recorded and neither is evaluated here.

Argument lists differ in shape between dialects, and the difference originates in the BNF rather than the generator: <fof_arguments> ::= <fof_term> | <fof_term>,<fof_arguments> nests to the right, while <tff_arguments> ::= <tff_term><comma_tff_term>* is flat. p(x, y, z) is therefore a two-child node in FOF and a three-child node in TFF, and counting children directly would give the FOF form an arity of two. The count recurses through children of the same kind instead, which is correct for both.