ShotDs.Data.Problem (shot_ds v1.2.10)

Copy Markdown View Source

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

axiom_input()

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).

conjecture_input()

A conjecture entry accepted by new/1. nil if no conjecture is given. A bare term_id gets the default name "conjecture".

new_opts()

Options accepted by new/1 and new!/1.

t()

A Problem is a collection holding the relevant information and meta-information of a problem stored in separate fields.

Functions

new(opts \\ [])

Builds a Problem struct from a list of axioms and an optional conjecture.

new!(opts \\ [])

Same as new/1 but raises ArgumentError on failure.

Types

axiom_input()

@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).

conjecture_input()

@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".

new_opts()

@type new_opts() :: [
  axioms: [axiom_input()],
  conjecture: conjecture_input(),
  path: String.t()
]

Options accepted by new/1 and new!/1.

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

new(opts \\ [])

@spec new(new_opts()) :: {:ok, t()} | {:error, String.t()}

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 of axiom_input() entries (default [])
  • :conjecture — conjecture_input() (default nil)
  • :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"

new!(opts \\ [])

@spec new!(new_opts()) :: t()

Same as new/1 but raises ArgumentError on failure.