@spec conjectures(Tptp.File.t() | Tptp.Unit.t()) :: [Tptp.Statement.Annotated.t()]

Returns the conjecture statements.

iex> {:ok, file, []} = Tptp.from_string("fof(a,axiom,p). fof(g,conjecture,q).")
iex> file |> Tptp.Query.conjectures() |> Enum.map(& &1.name.text)
["g"]

@spec dialect(Tptp.File.t() | Tptp.Unit.t()) :: dialect()

Returns the narrowest dialect admitting every construct in the file.

iex> {:ok, file, []} = Tptp.from_string("cnf(a, axiom, p | ~q).")
iex> Tptp.Query.dialect(file)
:cnf

iex> {:ok, file, []} = Tptp.from_string("tff(a, type, f: $i > $o). tff(b, axiom, f(a)).")
iex> Tptp.Query.dialect(file)
:tf0

iex> {:ok, file, []} = Tptp.from_string("thf(a, axiom, !! @ p).")
iex> Tptp.Query.dialect(file)
:th1

A !> that binds a term is a dependent type rather than a polymorphic one, which is DH0 or DH1 and not TH1:

iex> source = "thf(n, type, nat: $tType). thf(f, type, fin: nat > $tType)."
iex> {:ok, file, []} = Tptp.from_string(source)
iex> Tptp.Query.dialect(file)
:dh0

@spec dialects() :: [dialect()]

Returns the dialects in rank/1 order.

iex> Tptp.Query.dialects() |> Enum.take(3)
[:unknown, :cnf, :fof]

@spec features(Tptp.File.t() | Tptp.Unit.t()) :: [atom()]

Returns the features the file uses, as recorded by the lint traversal.

A type quantifier produces either :polymorphic or :dependent according to what it binds rather than to the quantifier itself; see Tptp.Lint.Collect.

Use this where the dialect alone is insufficiently specific. A consumer selecting a prover may need to know that a TF0 problem uses arithmetic, which does not affect its dialect.

iex> {:ok, file, []} = Tptp.from_string("thf(a, type, g: !>[A: $tType]: (A > A)).")
iex> file |> Tptp.Query.features() |> Enum.sort()
[:polymorphic, :thf, :typed]

@spec from_features(Enumerable.t()) :: dialect()

Returns the dialect implied by a set of features.

Separated from dialect/1 so that the mapping can be read and tested independently.

iex> Tptp.Query.from_features([:fof])
:fof
iex> Tptp.Query.from_features([:tff, :typed, :polymorphic])
:tf1

@spec rank(dialect()) :: non_neg_integer()

Returns a dialect's position in a stable listing order, approximately narrowest to widest.

Intended for ordering a table of dialects. Unlike within?/2 it is total, and it asserts nothing about containment: rank(:tcf) < rank(:tf1) determines their order in a report only.

iex> Tptp.Query.rank(:cnf) < Tptp.Query.rank(:th1)
true

@spec roles(Tptp.File.t() | Tptp.Unit.t()) :: %{required(binary()) => pos_integer()}

Returns the roles the file uses, with the number of statements carrying each.

iex> {:ok, file, []} = Tptp.from_string("fof(a,axiom,p). fof(b,axiom,q). fof(c,conjecture,r).")
iex> Tptp.Query.roles(file)
%{"axiom" => 2, "conjecture" => 1}

@spec symbols(Tptp.File.t() | Tptp.Unit.t()) :: %{
  required(binary()) => Tptp.Lint.Table.symbol()
}

Returns the symbol table without applying any rule.

The table constructed by Tptp.Lint, for consumers requiring the declarations and observed arities without the diagnostics.

Keyed by Tptp.Node.value/1, the atomic word, rather than by the spelling, so that 'p' and p are the single symbol the BNF defines them to be. A signature derived from this table inherits that identity; keying on the spelling instead yields two constants that never unify.

iex> {:ok, file, []} = Tptp.from_string("tff(t, type, 'p': $i > $o). tff(a, axiom, p(x)).")
iex> file |> Tptp.Query.symbols() |> Map.keys() |> Enum.sort()
["p", "x"]

@spec within?(dialect(), dialect()) :: boolean()

Returns whether every file of one dialect is also a file of another.

A partial order. The TPTP dialects are not linearly ordered: TCF is typed clause form, and TXF and the non-classical languages are separate branches, so there exist incomparable pairs. A TH1 file is not an NXF file and an NXF file is not a TH1 file.

iex> Tptp.Query.within?(:fof, :th0)
true
iex> Tptp.Query.within?(:th1, :fof)
false

iex> {Tptp.Query.within?(:th1, :nxf), Tptp.Query.within?(:nxf, :th1)}
{false, false}

Provenance

The vendored BNF does not state this relation. Each language has its own nonterminals and the grammar makes no claim about containment, so the relation is a hand-written table: @extends records immediate edges only and is closed transitively at compile time.

It is therefore a judgement of the same kind as the SZS isa hierarchy, which Tptp.Szs.Ontology declines to model. The distinction is the use to which the answer is put. An SZS precedence would constitute a claim about the meaning of a prover's result. This relation determines only which analyzers Tptp.Analyzer.run_all/3 offers a file to, where an error causes an analyzer to run that should have been skipped. An analyzer requiring no such inference can decline it; see Tptp.Analyzer.gate/0 and its {:exactly, dialects} form.

It is not a basis for deciding whether a given prover accepts a file.

Being partial, it is not a comparator. Use rank/1 for ordering.