nx_prover_a1.nx source
↩ module page · 220 lines · 8206 B
1// nx_prover_a1.nx -- Phase A1 extended-rule forward-chaining prover.
2//
3// Phase A0 (in nx_prover.nx) handled modus ponens only. Phase A1
4// adds four more rule families, dispatched per cycle:
5//
6// substitution (a = b) + P(a) -> P(b)
7// conjunction intro A + B -> A^B
8// conjunction elim A^B -> A (and A^B -> B)
9// disjunction intro A -> A v B (for declared OR-targets)
10//
11// All rules are declared as TABLES. The caller supplies:
12//
13// subst_table[i*3] = "lhs" stmt
14// subst_table[i*3+1] = "rhs" stmt (an equality A=B implies a=b)
15// subst_table[i*3+2] = "carrier" P(*) stmt
16//
17// conj_table[i*3] = A stmt
18// conj_table[i*3+1] = B stmt
19// conj_table[i*3+2] = A^B stmt
20//
21// The forward-chaining loop applies each rule family per cycle until
22// target found or no progress.
23//
24// Phase A1 still uses opaque i64 stmt_ids -- no internal structure
25// reasoning. Phase A2 will add typed terms + unification.
26//
27// genealogy_id: prawitz_natural_deduction_1965 + gentzen_sequent_1935
28// lineage_id: substitution + intro_elim_rules + forward_chaining
29// axioms: NX_AX_LOGIC_MODUS_PONENS_RULE + NX_DRULE_SUBSTITUTION
30// + NX_DRULE_CONJ_INTRO + NX_DRULE_CONJ_ELIM
31// + NX_DRULE_DISJ_INTRO
32
33// nx_safety_envelope:
34// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
35// sil_target: SIL1
36// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
37// verdict: NOT_YET_EVALUATED
38
39import "syscalls.nx"
40import "nx_axioms.nx"
41import "nx_derive.nx"
42import "nx_prover.nx"
43
44// ===== rule tables =====================================================
45//
46// Substitution rule: subst_table[i*3] = "a=b" equality stmt;
47// subst_table[i*3+1] = "P(a)" precondition;
48// subst_table[i*3+2] = "P(b)" conclusion.
49// If both equality and P(a) are derived, P(b) becomes derivable.
50
51func nx_a1_step_substitution(s: *ProofState, subst: *i64, n_subst: i64) -> i64 {
52 var i: i64 = 0
53 var added: i64 = 0
54 while i < n_subst {
55 let eq_stmt: i64 = subst[i * 3]
56 let p_a: i64 = subst[i * 3 + 1]
57 let p_b: i64 = subst[i * 3 + 2]
58 if nx_prover_has_stmt(s, eq_stmt) == 1 {
59 if nx_prover_has_stmt(s, p_a) == 1 {
60 if nx_prover_has_stmt(s, p_b) == 0 {
61 var eq_idx: i64 = -1
62 var pa_idx: i64 = -1
63 var j: i64 = 0
64 while j < s.n_facts {
65 let fj: *Fact = nx_prover_fact_at(s, j)
66 if fj.stmt_id == eq_stmt { eq_idx = j }
67 if fj.stmt_id == p_a { pa_idx = j }
68 j = j + 1
69 }
70 if eq_idx >= 0 {
71 if pa_idx >= 0 {
72 nx_prover_add_inferred(s, p_b,
73 NX_DRULE_SUBSTITUTION, pa_idx, eq_idx)
74 added = added + 1
75 }
76 }
77 }
78 }
79 }
80 i = i + 1
81 }
82 return added
83}
84
85// Conjunction introduction: conj_table[i*3] = A; +1 = B; +2 = AandB.
86// If both A and B are derived, AandB becomes derivable.
87
88func nx_a1_step_conj_intro(s: *ProofState, conj: *i64, n_conj: i64) -> i64 {
89 var i: i64 = 0
90 var added: i64 = 0
91 while i < n_conj {
92 let a: i64 = conj[i * 3]
93 let b: i64 = conj[i * 3 + 1]
94 let ab: i64 = conj[i * 3 + 2]
95 if nx_prover_has_stmt(s, a) == 1 {
96 if nx_prover_has_stmt(s, b) == 1 {
97 if nx_prover_has_stmt(s, ab) == 0 {
98 var a_idx: i64 = -1
99 var b_idx: i64 = -1
100 var j: i64 = 0
101 while j < s.n_facts {
102 let fj: *Fact = nx_prover_fact_at(s, j)
103 if fj.stmt_id == a { a_idx = j }
104 if fj.stmt_id == b { b_idx = j }
105 j = j + 1
106 }
107 if a_idx >= 0 {
108 if b_idx >= 0 {
109 nx_prover_add_inferred(s, ab,
110 NX_DRULE_CONJ_INTRO, a_idx, b_idx)
111 added = added + 1
112 }
113 }
114 }
115 }
116 }
117 i = i + 1
118 }
119 return added
120}
121
122// Conjunction elimination: conj_table[i*3] = A; +1 = B; +2 = AandB.
123// If AandB is derived, both A and B become derivable.
124
125func nx_a1_step_conj_elim(s: *ProofState, conj: *i64, n_conj: i64) -> i64 {
126 var i: i64 = 0
127 var added: i64 = 0
128 while i < n_conj {
129 let a: i64 = conj[i * 3]
130 let b: i64 = conj[i * 3 + 1]
131 let ab: i64 = conj[i * 3 + 2]
132 if nx_prover_has_stmt(s, ab) == 1 {
133 var ab_idx: i64 = -1
134 var j: i64 = 0
135 while j < s.n_facts {
136 let fj: *Fact = nx_prover_fact_at(s, j)
137 if fj.stmt_id == ab { ab_idx = j; j = s.n_facts }
138 j = j + 1
139 }
140 if ab_idx >= 0 {
141 if nx_prover_has_stmt(s, a) == 0 {
142 nx_prover_add_inferred(s, a, NX_DRULE_CONJ_ELIM, ab_idx, -1)
143 added = added + 1
144 }
145 if nx_prover_has_stmt(s, b) == 0 {
146 nx_prover_add_inferred(s, b, NX_DRULE_CONJ_ELIM, ab_idx, -1)
147 added = added + 1
148 }
149 }
150 }
151 i = i + 1
152 }
153 return added
154}
155
156// Disjunction introduction: disj_table[i*2] = A; +1 = AorB.
157// If A is derived, AorB becomes derivable.
158
159func nx_a1_step_disj_intro(s: *ProofState, disj: *i64, n_disj: i64) -> i64 {
160 var i: i64 = 0
161 var added: i64 = 0
162 while i < n_disj {
163 let a: i64 = disj[i * 2]
164 let ab: i64 = disj[i * 2 + 1]
165 if nx_prover_has_stmt(s, a) == 1 {
166 if nx_prover_has_stmt(s, ab) == 0 {
167 var a_idx: i64 = -1
168 var j: i64 = 0
169 while j < s.n_facts {
170 let fj: *Fact = nx_prover_fact_at(s, j)
171 if fj.stmt_id == a { a_idx = j; j = s.n_facts }
172 j = j + 1
173 }
174 if a_idx >= 0 {
175 nx_prover_add_inferred(s, ab, NX_DRULE_DISJ_INTRO, a_idx, -1)
176 added = added + 1
177 }
178 }
179 }
180 i = i + 1
181 }
182 return added
183}
184
185// Bundle: a complete A1 step applies ALL rule families.
186func nx_a1_step_all(s: *ProofState,
187 impl_table: *i64, n_impls: i64,
188 subst_table: *i64, n_subst: i64,
189 conj_table: *i64, n_conj: i64,
190 disj_table: *i64, n_disj: i64) -> i64 {
191 let mp: i64 = nx_prover_step_mp(s, impl_table, n_impls)
192 let sb: i64 = nx_a1_step_substitution(s, subst_table, n_subst)
193 let ci: i64 = nx_a1_step_conj_intro(s, conj_table, n_conj)
194 let ce: i64 = nx_a1_step_conj_elim(s, conj_table, n_conj)
195 let di: i64 = nx_a1_step_disj_intro(s, disj_table, n_disj)
196 return mp + sb + ci + ce + di
197}
198
199// Top-level A1 search: same shape as nx_prover_search but applies
200// the bundled rule families.
201func nx_prover_a1_search(s: *ProofState,
202 impl_table: *i64, n_impls: i64,
203 subst_table: *i64, n_subst: i64,
204 conj_table: *i64, n_conj: i64,
205 disj_table: *i64, n_disj: i64,
206 cycle_budget: i64) -> i64 {
207 if nx_prover_has_target(s) == 1 { return NX_PROVER_PROVED }
208 var cycles: i64 = 0
209 while cycles < cycle_budget {
210 let added: i64 = nx_a1_step_all(s, impl_table, n_impls,
211 subst_table, n_subst,
212 conj_table, n_conj,
213 disj_table, n_disj)
214 cycles = cycles + 1
215 s.cycle_count = cycles
216 if nx_prover_has_target(s) == 1 { return NX_PROVER_PROVED }
217 if added == 0 { return NX_PROVER_NO_RULES_APPLY }
218 }
219 return NX_PROVER_NOT_PROVED_BUDGET
220}