nx_sine.nx

nx_sine.nx -- Sine (Sumo INference Engine) axiom selection. Per Vampire-displacement roadmap Phase 2. Critical for the CASC LTB (Large Theory Batch) division -- problems may have thousands of axioms but the conjecture only needs a few dozen. Sine picks the relevant subset before saturation, often shrinking the search space by 100x or more. Hoder + Voronkov 2011 standard formulation: tolerance T (typically 1.0 to 3.0) For each symbol s in the problem, count freq(s) = number of axioms containing s. For each symbol s, the "D-relation" picks definitional axioms: d(s) = { axiom A : s ∈ symbols(A) ∧ freq(s) ≤ T * min { freq(t) : t ∈ symbols(A) } } Selection algorithm (fixpoint): selected = ∅ queue = symbols(conjecture) while queue not empty: s = pop(queue) for each A in d(s) not in selected: add A to selected add new symbols of A to queue return selected Output: subset of axioms reachable from the conjecture's symbols through definition chains. Bits-up nx_int, no f64. tolerance is Q10 (1024 = 1.0).