nx_prover.nx

buildroot/runtime/nx_prover.nx

8288 B236 linesdepth 4pulls 5 transitivereach 12 importersview sourcekind librarytopic prover

docs dependencies structs consts functions

about

nx_prover.nx -- substrate-native bounded forward-chaining proof search. No AI in the loop. No external prover. Deterministic BFS over the closed inference rules from nx_derive.nx, starting from axioms. Phase A0 capability: * Axiom-citation chains (target == cited axiom) * 1-step modus ponens (premise A and rule A->B in fact set) * Substitution chains (a=b and P(a) in fact set -> P(b)) * Bounded cycle + depth genealogy_id: gentzen_1935 (sequent calculus) + robinson_1965 (resolution) + wiedijk_qed_1994 (cross-verification vision) lineage_id: formal_proof_search + bounded_inference axioms: NX_AX_LOGIC_MODUS_PONENS_RULE, NX_AX_LOGIC_IDENTITY

dependencies 3 imports · 10 importers

imports: syscalls.nxnx_axioms.nxnx_derive.nx

imported by: nx_auto_verify.nxnx_auto_verify_test.nxnx_ingest_pipeline.nxnx_prover_a1.nxnx_prover_a1_test.nxnx_prover_eval.nxnx_prover_eval_test.nxnx_prover_test.nxnx_shard.nxnx_validation_cycle.nx

structs

43	struct Fact
54	struct ProofState

consts

29	const NX_PROVER_PROVED: i64 = 0
30	const NX_PROVER_NOT_PROVED_BUDGET: i64 = 1
31	const NX_PROVER_REFUTED: i64 = 2
32	const NX_PROVER_NO_RULES_APPLY: i64 = 3
52	const NX_FACT_BYTES: i64 = 48
63	const NX_PROVER_MAX_FACTS: i64 = 1024

functions

65	func nx_prover_state_alloc(target: i64) -> *ProofState called by 4: nx_auto_try_prove main nx_eval_run_case main
77	func nx_prover_fact_at(s: ProofState, i: i64) -> Fact called by 10: nx_prover_add_axiom nx_prover_add_inferred nx_prover_has_target nx_prover_has_stmt nx_prover_step_mp nx_prover_build_chain+4
82	func nx_prover_add_axiom(s: *ProofState, stmt_id: i64, axiom_code: i64) -> i64 called by 4: nx_auto_try_prove main nx_eval_run_case main calls 2: nx_axiom_is_valid nx_prover_fact_at
99	func nx_prover_add_inferred(s: *ProofState, stmt_id: i64, called by 5: nx_prover_step_mp nx_a1_step_substitution nx_a1_step_conj_intro nx_a1_step_conj_elim nx_a1_step_disj_intro calls 1: nx_prover_fact_at
127	func nx_prover_has_target(s: *ProofState) -> i64 called by 2: nx_prover_search nx_prover_a1_search calls 1: nx_prover_fact_at
142	func nx_prover_has_stmt(s: *ProofState, stmt: i64) -> i64 called by 5: nx_prover_step_mp nx_a1_step_substitution nx_a1_step_conj_intro nx_a1_step_conj_elim nx_a1_step_disj_intro calls 1: nx_prover_fact_at
168	func nx_prover_step_mp(s: ProofState, impl_table: i64, n_impls: i64) -> i64 called by 2: nx_prover_search nx_a1_step_all calls 3: nx_prover_has_stmt nx_prover_fact_at nx_prover_add_inferred
201	func nx_prover_search(s: ProofState, impl_table: i64, n_impls: i64, called by 3: nx_auto_try_prove nx_eval_run_case main calls 2: nx_prover_has_target nx_prover_step_mp
220	func nx_prover_build_chain(s: ProofState, chain: DerivationChain) -> i64 called by 1: main calls 4: nx_prover_fact_at nx_deriv_add_axiom nx_deriv_add_step nx_deriv_mark_theorem