A data structure to describe a (TPTP) proof problem.
It contains meta-information about the problem (path to proof file, included files) as well as the problem definition which consist of:
A map of types which maps symbols (user types or constants) to their type
The definitions given by the user
The axioms defined by the user
The conjecture to be proven based on the axioms and definitions
Note that definitions are not unfolded in the proof problem but kept as constants.
Summary
Types
A single axiom entry accepted by new/1. Either a {name, term_id} pair or
a bare term_id (in which case a name of the form "axiom_<n>" is generated
based on position).
A conjecture entry accepted by new/1. nil if no conjecture is given.
A bare term_id gets the default name "conjecture".
A Problem is a collection holding the relevant information and
meta-information of a problem stored in separate fields.
Functions
Builds a Problem struct from a list of axioms and an optional conjecture.
Same as new/1 but raises ArgumentError on failure.
Types
@type axiom_input() :: {String.t(), ShotDs.Data.Term.term_id()} | ShotDs.Data.Term.term_id()
A single axiom entry accepted by new/1. Either a {name, term_id} pair or
a bare term_id (in which case a name of the form "axiom_<n>" is generated
based on position).
@type conjecture_input() :: {String.t(), ShotDs.Data.Term.term_id()} | ShotDs.Data.Term.term_id() | nil
A conjecture entry accepted by new/1. nil if no conjecture is given.
A bare term_id gets the default name "conjecture".
@type new_opts() :: [ axioms: [axiom_input()], conjecture: conjecture_input(), path: String.t() ]
@type t() :: %ShotDs.Data.Problem{ axioms: [{String.t(), ShotDs.Data.Term.term_id()}], conjecture: {String.t(), ShotDs.Data.Term.term_id()} | nil, definitions: %{ required(ShotDs.Data.Declaration.t()) => ShotDs.Data.Term.term_id() }, includes: [String.t()], path: String.t(), types: %{ required(String.t()) => :base_type | ShotDs.Data.Type.t() | ShotDs.Data.TypeScheme.t() } }
A Problem is a collection holding the relevant information and
meta-information of a problem stored in separate fields.
The :path to a problem file is given as a string. This also includes the
paths to the included files in :includes.
The types are given as a map mapping symbol names (or type names) to their
defined types (can be :base_type for user-defined base types).
The definitions are given as a map from the symbol's name to the equation describing it. Note that the equation must first be deconstructed into the defined constant on the left hand side and it's definition on the right hand side.
The axioms are stored as a list of pairs containing the axiom's name as string and term as its corresponding ID.
The conjecture is tuple containing the conjecture's name as string and the
conjecture itself as the term's ID. The field's value is nil if no
conjecture could be found.
Functions
Builds a Problem struct from a list of axioms and an optional conjecture.
Axioms may be given as {name, term_id} pairs or as bare term_ids — bare
entries are auto-named "axiom_<n>" based on their position (1-indexed),
which is useful when the caller comes from an intermediate proof state where
the original names have been discarded. The conjecture may be given as
{name, term_id}, as a bare term_id (named "conjecture"), or as nil.
The types map is populated automatically by scanning all referenced terms:
- Each constant occurring in an axiom or conjecture is registered under
its name with a
ShotDs.Data.TypeScheme. When the same constant is used at multiple types (rank-1 polymorphism), the monotypes are reconciled by least-general-generalization and the free type variables are quantified in the resulting scheme. - Each user-defined base type atom (any goal other than
:o,:i, or:tType) is registered as:base_type.
Free variables that occur in only one formula retain their embedded types; when the problem is exported to TPTP, they are implicitly universally quantified in that formula (per the standard THF convention).
Free variables that occur in more than one formula (axioms and/or
conjecture) are automatically replaced everywhere by a fresh constant of the
same type so their sharing across formulas is preserved when the problem is
exported and re-parsed. The generated constant is named
"fv_" <> lowercased(fvar_name) — the fv_ prefix makes it visually
distinct from ordinary user constants — with a numeric suffix appended if
that name clashes with an existing constant.
Options
:axioms— list ofaxiom_input()entries (default[]):conjecture—conjecture_input()(defaultnil):path— display path for the constructed problem (default"memory")
Returns {:ok, problem} or {:error, reason}.
Examples
iex> import ShotDs.Hol.Definitions
iex> alias ShotDs.Stt.TermFactory, as: TF
iex> a_id = TF.make_const_term("a", type_i())
iex> p_id = TF.make_const_term("p", Type.new(:o, :i))
iex> ax = ShotDs.Hol.Dsl.app(p_id, a_id)
iex> {:ok, %ShotDs.Data.Problem{types: types}} =
...> ShotDs.Data.Problem.new(axioms: [{"ax1", ax}])
iex> Map.keys(types) |> Enum.sort()
["a", "p"]
iex> import ShotDs.Hol.Definitions
iex> alias ShotDs.Stt.TermFactory, as: TF
iex> a_id = TF.make_const_term("a", type_i())
iex> p_id = TF.make_const_term("p", Type.new(:o, :i))
iex> ax = ShotDs.Hol.Dsl.app(p_id, a_id)
iex> {:ok, problem} = ShotDs.Data.Problem.new(axioms: [ax], conjecture: ax)
iex> Enum.map(problem.axioms, &elem(&1, 0))
["axiom_1"]
iex> elem(problem.conjecture, 0)
"conjecture"Same as new/1 but raises ArgumentError on failure.