Tptp.Bnf.Vocabulary (Tptp v0.1.0)

Copy Markdown View Source

The closed vocabularies of the TPTP :== semantic layer.

DO NOT EDIT. Generated by mix tptp.gen from priv/bnf/SyntaxBNF-v9.3.1.3.

The grammar accepts far more than these lists do: <formula_role> ::= <lower_word> admits any lower word, and <defined_functor> ::= <atomic_defined_word> admits any $-word. Membership here is what separates a well-formed statement from a merely parseable one, and it is checked by Tptp.Lint at warning severity rather than by the parser.

Every list here is a :== rule of the BNF, with one exception. <reserved_word> is this library's own: the BNF has no such rule, and the list is every $-prefixed literal appearing in it.

Summary

Functions

Whether word is one of the 19 <defined_functor> values.

The 19 values the BNF lists for <defined_functor>.

Whether word is one of the 7 <defined_predicate> values.

The 7 values the BNF lists for <defined_predicate>.

Whether word is one of the 2 <defined_proposition> values.

The 2 values the BNF lists for <defined_proposition>.

Whether word is one of the 8 <defined_type> values.

The 8 values the BNF lists for <defined_type>.

Whether word is one of the 14 <formula_role> values.

The 14 values the BNF lists for <formula_role>.

Whether word is one of the 4 <intro_type> values.

The 4 values the BNF lists for <intro_type>.

Whether word is one of the 10 <ntf_connective_name> values.

The 10 values the BNF lists for <ntf_connective_name>.

Whether word is one of the 6 <ntf_logic_name> values.

The 6 values the BNF lists for <ntf_logic_name>.

Whether word is one of the 10 <ntf_modal_axiom> values.

The 10 values the BNF lists for <ntf_modal_axiom>.

Whether word is one of the 16 <ntf_modal_system> values.

The 16 values the BNF lists for <ntf_modal_system>.

Whether word is one of the 113 $-words the BNF mentions.

The 113 $-words the BNF mentions anywhere.

Whether word is one of the 34 <status_value> values.

The 34 values the BNF lists for <status_value>.

Functions

defined_functor?(word)

@spec defined_functor?(binary()) :: boolean()

Whether word is one of the 19 <defined_functor> values.

defined_functor_values()

@spec defined_functor_values() :: [binary()]

The 19 values the BNF lists for <defined_functor>.

defined_predicate?(word)

@spec defined_predicate?(binary()) :: boolean()

Whether word is one of the 7 <defined_predicate> values.

defined_predicate_values()

@spec defined_predicate_values() :: [binary()]

The 7 values the BNF lists for <defined_predicate>.

defined_proposition?(word)

@spec defined_proposition?(binary()) :: boolean()

Whether word is one of the 2 <defined_proposition> values.

defined_proposition_values()

@spec defined_proposition_values() :: [binary()]

The 2 values the BNF lists for <defined_proposition>.

defined_type?(word)

@spec defined_type?(binary()) :: boolean()

Whether word is one of the 8 <defined_type> values.

defined_type_values()

@spec defined_type_values() :: [binary()]

The 8 values the BNF lists for <defined_type>.

formula_role?(word)

@spec formula_role?(binary()) :: boolean()

Whether word is one of the 14 <formula_role> values.

formula_role_values()

@spec formula_role_values() :: [binary()]

The 14 values the BNF lists for <formula_role>.

intro_type?(word)

@spec intro_type?(binary()) :: boolean()

Whether word is one of the 4 <intro_type> values.

intro_type_values()

@spec intro_type_values() :: [binary()]

The 4 values the BNF lists for <intro_type>.

ntf_connective_name?(word)

@spec ntf_connective_name?(binary()) :: boolean()

Whether word is one of the 10 <ntf_connective_name> values.

ntf_connective_name_values()

@spec ntf_connective_name_values() :: [binary()]

The 10 values the BNF lists for <ntf_connective_name>.

ntf_logic_name?(word)

@spec ntf_logic_name?(binary()) :: boolean()

Whether word is one of the 6 <ntf_logic_name> values.

ntf_logic_name_values()

@spec ntf_logic_name_values() :: [binary()]

The 6 values the BNF lists for <ntf_logic_name>.

ntf_modal_axiom?(word)

@spec ntf_modal_axiom?(binary()) :: boolean()

Whether word is one of the 10 <ntf_modal_axiom> values.

ntf_modal_axiom_values()

@spec ntf_modal_axiom_values() :: [binary()]

The 10 values the BNF lists for <ntf_modal_axiom>.

ntf_modal_system?(word)

@spec ntf_modal_system?(binary()) :: boolean()

Whether word is one of the 16 <ntf_modal_system> values.

ntf_modal_system_values()

@spec ntf_modal_system_values() :: [binary()]

The 16 values the BNF lists for <ntf_modal_system>.

reserved_word?(word)

@spec reserved_word?(binary()) :: boolean()

Whether word is one of the 113 $-words the BNF mentions.

reserved_word_values()

@spec reserved_word_values() :: [binary()]

The 113 $-words the BNF mentions anywhere.

Not a :== rule — the BNF has no <reserved_word> — but every $-prefixed literal collected from every alternative of it. A superset of the words the language defines, which is what Tptp.Lint.Rules.DefinedWord wants.

status_value?(word)

@spec status_value?(binary()) :: boolean()

Whether word is one of the 34 <status_value> values.

status_value_values()

@spec status_value_values() :: [binary()]

The 34 values the BNF lists for <status_value>.