nx_resolution.nx

buildroot/runtime/nx_resolution.nx

5521 B155 linesdepth 5pulls 5 transitivereach 58 importersview sourcekind library

docs dependencies structs consts functions

about

nx_resolution.nx -- binary resolution rule (CASC proof-search core). Per user 2026-05-14: bits-up path to CASC win. This is THE rule Vampire / Otter / SPASS / SETHEO use thousands of times per second inside their saturation loops. Robinson 1965, extended via unification (built in nx_unify.nx). Literal: sign (POS=1 or NEG=-1) + atom (a Term). Clause: disjunction of literals; represented as flat array. Resolution rule: Given C1 = L1 v ... v Lm with literal Li = (sign_i, atom_i) And C2 = M1 v ... v Mn with literal Mj = (sign_j, atom_j) Where sign_i == -sign_j AND unify(atom_i, atom_j) succeeds with sigma, The resolvent is (C1 \ {Li} u C2 \ {Mj})[sigma]. nx_safety_envelope: intended_use: "Binary resolution -- first-order theorem prover step; substrate's competition-target against Vampire and friends" sil_target: SIL2 (proof system correctness) asil_target: QM dal_target: DAL B evidence: [Robinson_1965_canonical_basis, no_FP, sealed_clause_status_enum, unify_inheritance] hazard_register: [bug-tape-unfair-strategy-incompleteness, bug-tape-clause-bloat-OOM] residual_risk: "Resolution is refutation-complete; clause selection strategy determines termination behavior. Caller sets given-clause budget." verdict: NOT_YET_EVALUATED

dependencies 5 imports · 58 importers

diagram shows first 10 each side; +0 more imports, +48 more importers in the complete lists below.

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nx

imported by: nx_answer.nxnx_answer_test.nxnx_avatar_encode.nxnx_avatar_encode_test.nxnx_avatar_solve_test.nxnx_avatar_split.nxnx_avatar_split_test.nxnx_backward_subsume_test.nxnx_casc_bench.nxnx_casc_runner_test.nxnx_clause_components.nxnx_clause_components_test.nxnx_clause_weight_test.nxnx_demodulation.nxnx_demodulation_test.nxnx_discount_test.nxnx_eq_factor.nxnx_eq_factor_test.nxnx_fmb.nxnx_fmb_test.nxnx_fof_cnf.nxnx_fof_cnf_test.nxnx_fof_tseitin.nxnx_fof_tseitin_test.nxnx_hyperres.nxnx_hyperres_test.nxnx_indexed_subsume_test.nxnx_inst_gen.nxnx_inst_gen_test.nxnx_paramodulation.nxnx_paramodulation_test.nxnx_pre_sat.nxnx_pre_sat_test.nxnx_pure_lit.nxnx_pure_lit_test.nxnx_resolution_test.nxnx_saturation.nxnx_saturation_test.nxnx_selection.nxnx_selection_test.nxnx_sine.nxnx_sine_test.nxnx_solve.nxnx_solve_test.nxnx_subsumption.nxnx_subsumption_test.nxnx_tautology.nxnx_tautology_test.nxnx_tptp_emit.nxnx_tptp_emit_test.nxnx_tptp_formula.nxnx_tptp_formula_test.nxnx_tptp_load.nxnx_tptp_load_any.nxnx_tptp_load_test.nxnx_tptp_write_test.nxnx_tstp_emit.nxnx_tstp_emit_test.nx

structs

43	struct Literal
74	struct Clause

consts

40	const NX_LIT_POS: nx_int = 1
41	const NX_LIT_NEG: nx_int = -1
48	const NX_LITERAL_BYTES: nx_int = 16
72	const NX_CLAUSE_MAX_LITS: nx_int = 64
79	const NX_CLAUSE_BYTES: nx_int = 16

functions

50	func nx_lit_make(sign: nx_int, atom: Term) -> Literal called by 42: nx_answer_lit main nx_avatar_neg_sp main main main+36 calls 1: sys_mmap
58	func nx_lit_apply_subst(l: Literal, s: Subst) -> *Literal called by 6: nx_eq_factor nx_hyperresolve nx_inst_apply_clause nx_paramodulate nx_resolve nx_factor calls 2: nx_subst_apply nx_lit_make
64	func nx_lit_complementary_head(l1: Literal, l2: Literal) -> nx_int
81	func nx_clause_new() -> *Clause called by 39: main main main main mk_p1 mk_p2+33 calls 1: sys_mmap
88	func nx_clause_lit_at(c: Clause, i: nx_int) -> Literal called by 41: nx_clause_is_answer_only nx_clause_extract_answer nx_avatar_encode_to_sat main nx_avatar_split_clause nx_clause_components_classify+35
92	func nx_clause_add(c: Clause, l: Literal) -> *NxResult called by 46: nx_answer_attach main nx_avatar_encode_to_sat main nx_avatar_split_clause main+40 calls 3: nx_result_err nx_clause_lit_at nx_result_ok
107	func nx_resolve(c1: *Clause, i: nx_int, called by 3: main nx_sat_try_resolve_pair nx_sat_try_resolve_pair_filtered calls 8: nx_result_err nx_clause_lit_at nx_subst_new nx_unify nx_result_is_err nx_lit_apply_subst+2
152	func nx_clause_is_empty(c: *Clause) -> nx_int called by 4: main nx_sat_try_resolve_pair nx_sat_try_paramodulate_pair_filtered nx_sat_try_resolve_pair_filtered