nx_paramodulation.nx

nx_paramodulation.nx -- paramodulation rule for equational reasoning. Per Vampire-displacement roadmap Phase 2. The third corner of the equational-reasoning triangle (resolution + demodulation + paramodulation). Where demodulation rewrites with already-oriented equations, paramodulation derives new clauses by unifying a positive equality literal in one clause with a non-variable subterm in another clause, then rewriting under the unifier. Robinson + Wos 1969 standard formulation: Given: C ∨ s = t (clause with positive equality literal) D ∨ L[s'] (clause with subterm s' inside literal L) unify(s, s') = σ Derive: (C ∨ D ∨ L[t])σ where L[s' := t] is L with the chosen subterm position replaced by t, and everything is closed under σ. API: caller picks the equation literal (in eq_clause) and the target literal (in target_clause) by index; this primitive walks the target atom outermost-first looking for the first unifiable subterm. Returns null if no paramodulant exists for that literal pair. Bits-up nx_int. Variables shared across the two input clauses require renaming by the caller for soundness in saturation; this primitive trusts its inputs are appropriately renamed (matches nx_resolve's contract). nx_safety_envelope: intended_use: "Paramodulation inference rule -- equality reasoning in first-order theorem prover" sil_target: SIL2 asil_target: QM dal_target: DAL B evidence: [Robinson_Wos_1969_canonical_basis, composes_nx_unify_Result_typed, no_FP] hazard_register: [bug-tape-paramod-into-variable-position,