Tptp.Lint.Rules.Parent (Tptp v0.1.0)

Copy Markdown View Source

An inference record naming a parent absent from the unit.

In a derivation, inference(rule, [], [a, b]) records that the formula was derived from a and b. An absent parent renders the derivation uncheckable, indicating either a dropped statement or an incorrect name.

A warning, reported only for names occurring in formula-name position. A <source> is a <dag_source>, an <internal_source>, an <external_source>, the literal unknown, or a bracketed list of sources, and <name> is reachable through more than one of these: the rule of an <inference_record> and the file name of a <file_source> are not formula names and are not resolved as such. Neither is the literal unknown, which the grammar reads as a <name> — the first of Tptp.Bnf.Generator's departures — and which is therefore never reported as a missing parent. The rule also declines unless the unit names at least one formula, so it reports nothing for a problem containing no derivation.

Before v9.3.1.2 a <source> was a <general_term>, which admitted anything at all in the position this rule resolves.