ShotTx.Prover.Paramodulation (ShotTx v0.0.1)

Copy Markdown View Source

Utility helpers for term-DAG traversal used by ShotTx.Prover.Demodulation.

Why this module no longer performs paramodulation

Classical paramodulation derives a new formula by unifying an equation LHS with a subterm of a target literal, producing σ that binds variables on either side, and applying σ to the whole paramodulant. In ShotTx's rigid-variable tableau architecture that is unsound as a branch-level rule: γ-instantiation placeholders are free variables that ShotTx.Prover.ContradictionAgent reconciles globally via a CSP. Any branch-level σ commitment can:

  • Close a branch under a σ inconsistent with the σ CA eventually chooses (unsoundness on that branch), or
  • Pre-constrain CA's search space (loss of completeness).

Both structural (identity-based) and unifying paramodulation therefore moved out of this module. Equational rewriting that produces no variable binding — i.e. cases where the matcher σ is empty — is handled by ShotTx.Prover.Demodulation in canonicalizing form. Cases that genuinely require binding are left to Leibniz/extensional α-expansion, which produces new atomic literals that check_local_clashes reports as unification-based clashes to CA — the correct place for σ commitments.

What remains here

Pure term-DAG traversal helpers reused by demodulation:

  • subterms/1 — every subterm id reachable from a root.
  • applied_subterms/1 — subterms whose outermost form is h(a₁,…,aₙ) (used for head-position η-expansion rewriting in Demodulation).
  • replace_subterm/3 — DAG rewrite of every occurrence of a target subterm by a replacement.

Summary

Functions

applied_subterms(term_id)

All subterms of term_id that are applied terms whose outermost form is not an abstraction (i.e. bvars == [] and args != []).

replace_subterm(term_id, target, replacement)

Returns term_id with every occurrence of the subterm target replaced by replacement.

subterms(term_id)

Returns the set of all subterm ids that appear inside term_id, including term_id itself.

Functions

applied_subterms(term_id)

@spec applied_subterms(ShotDs.Data.Term.term_id()) ::
  MapSet.t(ShotDs.Data.Term.term_id())

All subterms of term_id that are applied terms whose outermost form is not an abstraction (i.e. bvars == [] and args != []).

Public so ShotTx.Prover.Demodulation can iterate them for head-position rewriting via primitive η-expansion equations.

replace_subterm(term_id, target, replacement)

@spec replace_subterm(
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id()
) :: ShotDs.Data.Term.term_id()

Returns term_id with every occurrence of the subterm target replaced by replacement.

subterms(term_id)

@spec subterms(ShotDs.Data.Term.term_id()) :: MapSet.t(ShotDs.Data.Term.term_id())

Returns the set of all subterm ids that appear inside term_id, including term_id itself.

Heads are not separately represented as term-id nodes; they only count as subterms when they appear as zero-arity terms. To rewrite at head positions see applied_subterms/1 and ShotTx.Prover.Demodulation.