nx_resolution.nx source
↩ module page · 155 lines · 5521 B
1// nx_resolution.nx -- binary resolution rule (CASC proof-search core).
2//
3// Per user 2026-05-14: bits-up path to CASC win. This is THE rule
4// Vampire / Otter / SPASS / SETHEO use thousands of times per second
5// inside their saturation loops. Robinson 1965, extended via
6// unification (built in nx_unify.nx).
7//
8// Literal: sign (POS=1 or NEG=-1) + atom (a Term).
9// Clause: disjunction of literals; represented as flat array.
10//
11// Resolution rule:
12// Given C1 = L1 v ... v Lm with literal Li = (sign_i, atom_i)
13// And C2 = M1 v ... v Mn with literal Mj = (sign_j, atom_j)
14// Where sign_i == -sign_j AND unify(atom_i, atom_j) succeeds with sigma,
15// The resolvent is (C1 \ {Li} u C2 \ {Mj})[sigma].
16//
17// nx_safety_envelope:
18// intended_use: "Binary resolution -- first-order theorem
19// prover step; substrate's competition-target
20// against Vampire and friends"
21// sil_target: SIL2 (proof system correctness)
22// asil_target: QM
23// dal_target: DAL B
24// evidence: [Robinson_1965_canonical_basis, no_FP,
25// sealed_clause_status_enum,
26// unify_inheritance]
27// hazard_register: [bug-tape-unfair-strategy-incompleteness,
28// bug-tape-clause-bloat-OOM]
29// residual_risk: "Resolution is refutation-complete; clause
30// selection strategy determines termination
31// behavior. Caller sets given-clause budget."
32// verdict: NOT_YET_EVALUATED
33
34import "nx_syscalls.nx"
35import "nx_runtime.nx"
36import "nx_tier.nx"
37import "nx_result.nx"
38import "nx_unify.nx"
39
40const NX_LIT_POS: nx_int = 1
41const NX_LIT_NEG: nx_int = -1
42
43struct Literal {
44 sign: nx_int,
45 atom: *Term,
46}
47
48const NX_LITERAL_BYTES: nx_int = 16
49
50func nx_lit_make(sign: nx_int, atom: *Term) -> *Literal {
51 let l: *Literal = (sys_mmap(NX_LITERAL_BYTES as i64)) as *Literal
52 l.sign = sign
53 l.atom = atom
54 return l
55}
56
57// Apply substitution to a literal.
58func nx_lit_apply_subst(l: *Literal, s: *Subst) -> *Literal {
59 let new_atom: *Term = nx_subst_apply(l.atom, s)
60 return nx_lit_make(l.sign, new_atom)
61}
62
63// Are two literals complementary (opposite sign + same atom symbol)?
64func nx_lit_complementary_head(l1: *Literal, l2: *Literal) -> nx_int {
65 if l1.sign != (0 - l2.sign) { return 0 }
66 if l1.atom.sym != l2.atom.sym { return 0 }
67 if l1.atom.kind != l2.atom.kind { return 0 }
68 return 1
69}
70
71// ===== Clause = disjunction of literals =============================
72const NX_CLAUSE_MAX_LITS: nx_int = 64
73
74struct Clause {
75 n_lits: nx_int,
76 lits: *Literal, // flat array of Literal structs
77}
78
79const NX_CLAUSE_BYTES: nx_int = 16
80
81func nx_clause_new() -> *Clause {
82 let c: *Clause = (sys_mmap(NX_CLAUSE_BYTES as i64)) as *Clause
83 c.n_lits = 0
84 c.lits = (sys_mmap((NX_CLAUSE_MAX_LITS * NX_LITERAL_BYTES) as i64)) as *Literal
85 return c
86}
87
88func nx_clause_lit_at(c: *Clause, i: nx_int) -> *Literal {
89 return ((c.lits as nx_int) + (i * NX_LITERAL_BYTES)) as *Literal
90}
91
92func nx_clause_add(c: *Clause, l: *Literal) -> *NxResult {
93 if c.n_lits >= NX_CLAUSE_MAX_LITS { return nx_result_err(NX_ERR_INVALID_STATE) }
94 let slot: *Literal = nx_clause_lit_at(c, c.n_lits)
95 slot.sign = l.sign
96 slot.atom = l.atom
97 c.n_lits = c.n_lits + 1
98 return nx_result_ok(c.n_lits)
99}
100
101// ===== Binary resolution rule =======================================
102// Resolves clause c1 (at literal index i) with clause c2 (at literal
103// index j). Builds the resolvent in c_out (caller allocated).
104// Returns Result<n_resolvent_lits, NX_ERR_*>.
105//
106// Caller must have called nx_clause_new() on c_out; it will be filled.
107func nx_resolve(c1: *Clause, i: nx_int,
108 c2: *Clause, j: nx_int,
109 c_out: *Clause) -> *NxResult {
110 if i < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
111 if i >= c1.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
112 if j < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
113 if j >= c2.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
114
115 let l1: *Literal = nx_clause_lit_at(c1, i)
116 let l2: *Literal = nx_clause_lit_at(c2, j)
117
118 // Literals must be complementary (opposite signs).
119 if l1.sign != (0 - l2.sign) { return nx_result_err(NX_ERR_TAG_MISMATCH) }
120
121 // Unify the atoms.
122 let s: *Subst = nx_subst_new()
123 let r_un: *NxResult = nx_unify(l1.atom, l2.atom, s)
124 if nx_result_is_err(r_un) == 1 { return r_un }
125
126 // Build resolvent: all literals from c1 except i, all from c2 except j,
127 // each with the substitution applied.
128 var k: nx_int = 0
129 while k < c1.n_lits {
130 if k != i {
131 let lk: *Literal = nx_clause_lit_at(c1, k)
132 let lk_subst: *Literal = nx_lit_apply_subst(lk, s)
133 let r: *NxResult = nx_clause_add(c_out, lk_subst)
134 if nx_result_is_err(r) == 1 { return r }
135 }
136 k = k + 1
137 }
138 k = 0
139 while k < c2.n_lits {
140 if k != j {
141 let lk: *Literal = nx_clause_lit_at(c2, k)
142 let lk_subst: *Literal = nx_lit_apply_subst(lk, s)
143 let r: *NxResult = nx_clause_add(c_out, lk_subst)
144 if nx_result_is_err(r) == 1 { return r }
145 }
146 k = k + 1
147 }
148 return nx_result_ok(c_out.n_lits)
149}
150
151// Is this clause empty? Empty clause = contradiction = UNSAT proof.
152func nx_clause_is_empty(c: *Clause) -> nx_int {
153 if c.n_lits == 0 { return 1 }
154 return 0
155}