Tableau rule classification and priority costs.
classify_formula/3 inspects a term-id and dispatches it to one of the
tableau rule variants (α, β, γ, γ-finite, δ, prim-subst, equality
expansion, rename, instantiate, atomic, tautology, contradiction). The
classifier is polarity-aware — negated formulas are routed through
classify_neg_formula/3 — and honours two Parameters knobs:
finite_o_quantification— whentrue,∀x^o. …is handled by the finite γ-rule (full enumeration of the propositional domain) instead of the ordinary γ-rule.equivalence_processing— chooses between same-polarity β-split, α-form via bidirectional implication, or a hybrid:dualform.
rule_cost/1,2 maps a classified rule to a priority in the FormulaPqueue
(lower = higher priority). resolve_cost_strategy/1 converts a named
strategy (:default, :uniform, :depth_first, {:custom, fun}) into a
concrete cost function — used by the ablation sweep so parameter files
stay self-describing.
Summary
Types
An alpha-rule decomposes the formula linearly into a list of formulas.
Formulas not matching any of the rules above are considered atomic and can for example be processed with unification.
A beta-rule decomposes the formula into two tuples corresponding to branches.
A contradiction trivially closes the tableau branch.
Partial override map for rule_cost/2. Any kind absent from the map keeps
its default. Keys not recognised by the rule case are ignored.
A delta rule instantiates an existentially quantified predicate with a skolem term dependent on the predicates free variables.
Equality expansion rule. Mechanically identical to an α-rule (a linear
decomposition into a list of produced formulas), but tagged with its
equality_kind so the cost function can charge each kind separately and
proof-search can de-prioritize Leibniz behind paramodulation.
Discriminates the three flavors of equality expansion.
Selects how equivalence (↔) is expanded.
Rule for consuming a gamma-formula when the domain is finite.
A gamma rule instantiates a universally quantified predicate with a fresh variable. As this rule is not consumed due to completeness, the second element of the tuple corresponds to the recipe for instantiations, i.e., a formula accepting a fresh variable. The third field captures the type of the variable. The last field keeps track of the rule instantiations for that formula so far.
This produces a lazy stream of {instantiated_term, corresponding_def} if the
(rename)-rule is not applicable and one of the arguments is an o-type that
can be instantiated. Additionally captures the number of instances.
Primitive substitution rule. Instantiates a universally quantified formula with general bindings that fix a logical head symbol while leaving sub-formula positions as fresh holes. Fields: recipe, element type, current binding depth, and a progress map recording consumed base bindings and covered types at the current depth.
For introducing extensionality, complex argument terms are renamed with a fresh constant. The tuple in the second field captures the term with the renamed constant as its first argument and an equality serving as the context as its second argument.
Synthetic rule spliced by SuggestionAgent: apply recipe to term and
insert the result on the current branch. Unlike :instantiate, this does
not spawn a child branch — it is a hint, not a decomposition.
A tautology disregards the formula as it doesn't add information.
Functions
Classifies a term ID as the tableau rule that should be applied to it.
Resolves a formula_cost_strategy value from Parameters into the cost
function used by FormulaPqueue. Used by ablation sweeps to select a named
cost function without threading a lambda through the config.
Returns the priority cost for a rule; lower cost means higher priority in
the queue. Equivalent to rule_cost(rule, %{}).
Returns the priority cost for a rule, allowing per-kind overrides for
equality expansion. The overrides map only needs to mention the kinds
whose default should change; unlisted kinds keep their defaults.
Types
@type alpha_t() :: {:alpha, [ShotDs.Data.Term.term_id(), ...]}
An alpha-rule decomposes the formula linearly into a list of formulas.
@type atomic_t() :: {:atomic, ShotDs.Data.Term.term_id()}
Formulas not matching any of the rules above are considered atomic and can for example be processed with unification.
@type beta_t() :: {:beta, {ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()}}
A beta-rule decomposes the formula into two tuples corresponding to branches.
@type contradiction_t() :: :contradiction
A contradiction trivially closes the tableau branch.
@type cost_overrides() :: %{optional(equality_kind()) => non_neg_integer()}
Partial override map for rule_cost/2. Any kind absent from the map keeps
its default. Keys not recognised by the rule case are ignored.
@type delta_t() :: {:delta, ShotDs.Data.Term.term_id()}
A delta rule instantiates an existentially quantified predicate with a skolem term dependent on the predicates free variables.
@type equality_expansion_t() :: {:equality_expansion, equality_kind(), [ShotDs.Data.Term.term_id(), ...]}
Equality expansion rule. Mechanically identical to an α-rule (a linear
decomposition into a list of produced formulas), but tagged with its
equality_kind so the cost function can charge each kind separately and
proof-search can de-prioritize Leibniz behind paramodulation.
@type equality_kind() :: :iff_o | :extensional | :leibniz
Discriminates the three flavors of equality expansion.
:iff_o— equality at typeois just↔.:extensional— equality at a functional type expands via extensional equality (or, for closed sides, a fresh-constant application form).:leibniz— equality at any remaining type expands via the Leibniz schema∀P. P(a) ↔ P(b). The expensive one for FO.
@type equivalence_mode() :: :same_polarity | :bidirectional_imp | :dual
Selects how equivalence (↔) is expanded.
:same_polarity— current default. Positivep ↔ qβ-splits into{p ∧ q, ¬p ∧ ¬q}; negative¬(p ↔ q)β-splits into{¬p ∧ q, ¬q ∧ p}.:bidirectional_imp— rewritesp ↔ qas(p → q) ∧ (q → p). Positive becomes an α producing both implications; negative becomes a β over the two negated implications.:dual— emits both forms in a single α, so the prover can exploit either expansion. Positive:[p → q, q → p, (p ∧ q) ∨ (¬p ∧ ¬q)]; negative:[¬(p → q) ∨ ¬(q → p), (¬p ∧ q) ∨ (¬q ∧ p)].
@type gamma_finite_t() :: {:gamma_finite, ShotDs.Data.Term.term_id(), ShotDs.Data.Type.t()}
Rule for consuming a gamma-formula when the domain is finite.
@type gamma_t() :: {:gamma, ShotDs.Data.Term.term_id(), ShotDs.Data.Type.t(), non_neg_integer(), boolean()}
A gamma rule instantiates a universally quantified predicate with a fresh variable. As this rule is not consumed due to completeness, the second element of the tuple corresponds to the recipe for instantiations, i.e., a formula accepting a fresh variable. The third field captures the type of the variable. The last field keeps track of the rule instantiations for that formula so far.
@type instantiate_t() :: {:instantiate, Enumerable.t({ShotDs.Data.Term.term_id(), definition_t()}), pos_integer()}
This produces a lazy stream of {instantiated_term, corresponding_def} if the
(rename)-rule is not applicable and one of the arguments is an o-type that
can be instantiated. Additionally captures the number of instances.
@type prim_subst_t() :: {:prim_subst, ShotDs.Data.Term.term_id(), ShotDs.Data.Type.t(), pos_integer(), prim_subst_progress()}
Primitive substitution rule. Instantiates a universally quantified formula with general bindings that fix a logical head symbol while leaving sub-formula positions as fresh holes. Fields: recipe, element type, current binding depth, and a progress map recording consumed base bindings and covered types at the current depth.
@type rename_t() :: {:rename, {ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()}}
For introducing extensionality, complex argument terms are renamed with a fresh constant. The tuple in the second field captures the term with the renamed constant as its first argument and an equality serving as the context as its second argument.
@type rule_t() :: alpha_t() | beta_t() | gamma_t() | gamma_finite_t() | delta_t() | prim_subst_t() | tautology_t() | contradiction_t() | rename_t() | instantiate_t() | atomic_t() | equality_expansion_t() | suggested_instantiate_t()
@type suggested_instantiate_t() :: {:suggested_instantiate, recipe :: ShotDs.Data.Term.term_id(), term :: ShotDs.Data.Term.term_id()}
Synthetic rule spliced by SuggestionAgent: apply recipe to term and
insert the result on the current branch. Unlike :instantiate, this does
not spawn a child branch — it is a hint, not a decomposition.
@type tautology_t() :: :tautology
A tautology disregards the formula as it doesn't add information.
Functions
@spec classify_formula(ShotDs.Data.Term.term_id(), boolean(), equivalence_mode()) :: rule_t()
Classifies a term ID as the tableau rule that should be applied to it.
The second argument controls how quantifiers over pure o-types are
handled. When true (default) they are routed to the finite γ-rule which
enumerates the propositional domain; when false they fall through to the
ordinary γ-rule, the same path used for non-o quantifiers.
The third argument selects an equivalence expansion strategy; see
equivalence_mode/0.
@spec resolve_cost_strategy( :default | :uniform | :depth_first | {:custom, (rule_t() -> non_neg_integer())} ) :: (rule_t() -> non_neg_integer())
Resolves a formula_cost_strategy value from Parameters into the cost
function used by FormulaPqueue. Used by ablation sweeps to select a named
cost function without threading a lambda through the config.
:default—rule_cost/1(the historical default).:uniform— every rule has cost1; the queue degenerates to FIFO insertion order, giving a breadth-first-ish enumeration.:depth_first— cheap linear decompositions (:alpha,:atomic,:tautology,:contradiction) stay small; branching rules (:beta,:prim_subst,:gamma,:instantiate) are pushed to the back so a single branch is developed as deep as possible before splitting.{:custom, fun}— usefundirectly.
@spec rule_cost(rule_t()) :: non_neg_integer()
Returns the priority cost for a rule; lower cost means higher priority in
the queue. Equivalent to rule_cost(rule, %{}).
@spec rule_cost(rule_t(), cost_overrides()) :: non_neg_integer()
Returns the priority cost for a rule, allowing per-kind overrides for
equality expansion. The overrides map only needs to mention the kinds
whose default should change; unlisted kinds keep their defaults.
Typical use is to pin a heavy cost on Leibniz expansion while letting the o-type and extensional forms stay cheap:
formula_cost: &ShotTx.Prover.Rules.rule_cost(&1, %{leibniz: 100})