# `ShotDs.Data.Problem`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/data/problem.ex#L1)

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.

# `t`

```elixir
@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()}
}
```

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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*