nx_prove_propositional.nx
buildroot/runtime/nx_prove_propositional.nx
about
nx_prove_propositional.nx -- AUTO-PROVER ENGINE
Per user 2026-05-15: "build the system or engine that does this
this goes for all nishilang ... make sure it exceeds or matches
everything wikipedia called out on proofs that are required".
dependencies 1 imports · 3 importers
imports: nx_kernel_v2.nx
imported by: nx_prove_propositional_test.nxnx_tactics.nxnx_world_demo_test.nx
structs
| 18 | struct ProofCtx |
consts
| 15 | const NX_PROVE_MAX_CTX: nx_int = 64 |
| 16 | const NX_PROVE_MAX_DEPTH: nx_int = 16 |
| 23 | const NX_PROOF_CTX_BYTES: nx_int = 24 |
functions
| 25 | func nx_proof_ctx_new() -> *ProofCtx |
| 33 | func nx_proof_ctx_push(p: *ProofCtx, idx: nx_int) -> nx_int |
| 40 | func nx_proof_ctx_pop(p: *ProofCtx) -> nx_int called by 1: nx_prove_aux |
| 45 | func nx_proof_ctx_seed(p: *ProofCtx, idxs: *nx_int, n: nx_int) -> nx_int |
| 56 | func nx_prove_ctx_lookup(ch: *K2Chain, p: *ProofCtx, goal: *Term) -> nx_int |
| 68 | func nx_prove_aux(ch: *K2Chain, p: *ProofCtx, goal: *Term, depth: nx_int) -> nx_int; |
| 69 | func nx_prove_false(ch: *K2Chain, p: *ProofCtx, depth: nx_int) -> nx_int; called by 1: nx_prove_aux |
| 71 | func nx_prove_and_elim_scan(ch: *K2Chain, p: *ProofCtx, goal: *Term) -> nx_int called by 1: nx_prove_aux calls 6: nx_k2_atnx_term_argnx_term_eqnx_k2_and_elim_lnx_proof_ctx_pushnx_k2_and_elim_r |
| 102 | func nx_prove_mp_scan(ch: *K2Chain, p: *ProofCtx, goal: *Term, depth: nx_int) -> nx_int called by 1: nx_prove_aux calls 6: nx_k2_atnx_term_argnx_term_eqnx_prove_auxnx_k2_modus_ponensnx_proof_ctx_push |
| 129 | func nx_prove_false(ch: *K2Chain, p: *ProofCtx, depth: nx_int) -> nx_int |
| 172 | func nx_prove_aux(ch: *K2Chain, p: *ProofCtx, goal: *Term, depth: nx_int) -> nx_int called by 1: nx_tac_auto calls 15: nx_prove_ctx_lookupnx_term_argnx_prove_auxnx_k2_and_intronx_proof_ctx_pushnx_k2_assume+9 |
| 277 | func nx_prove(ch: *K2Chain, axioms: *nx_int, n_ax: nx_int, goal: *Term) -> nx_int |