nx_proof_methods.nx
buildroot/runtime/nx_proof_methods.nx
about
nx_proof_methods.nx -- comprehensive sealed enum of proof methods
covering Wikipedia "Mathematical proof" + ATP technique families.
Per user 2026-05-14: substrate must cover every reasonable proof
method from the literature and bridge entry-level to advanced math.
dependencies 5 imports · 1 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_axioms.nxnx_derive.nx
imported by: nx_proofs_comprehensive.nx
structs
| none |
consts
| 21 | const NX_PROOF_METHOD_DIRECT: nx_int = 1 |
| 22 | const NX_PROOF_METHOD_INDUCTION: nx_int = 2 // weak/standard |
| 23 | const NX_PROOF_METHOD_INDUCTION_STRONG: nx_int = 3 // strong/complete |
| 24 | const NX_PROOF_METHOD_INDUCTION_STRUCT: nx_int = 4 // structural |
| 25 | const NX_PROOF_METHOD_INFINITE_DESCENT: nx_int = 5 // Fermat-style |
| 26 | const NX_PROOF_METHOD_CONTRAPOSITION: nx_int = 6 |
| 27 | const NX_PROOF_METHOD_CONTRADICTION: nx_int = 7 // reductio |
| 28 | const NX_PROOF_METHOD_CONSTRUCTION: nx_int = 8 // constructive existence |
| 29 | const NX_PROOF_METHOD_EXHAUSTION: nx_int = 9 // case analysis |
| 30 | const NX_PROOF_METHOD_CLOSED_CHAIN: nx_int = 10 // pairwise equivalence |
| 31 | const NX_PROOF_METHOD_PROBABILISTIC: nx_int = 11 |
| 32 | const NX_PROOF_METHOD_COMBINATORIAL: nx_int = 12 // bijection / double-count |
| 33 | const NX_PROOF_METHOD_NONCONSTRUCTIVE: nx_int = 13 |
| 34 | const NX_PROOF_METHOD_COMPUTER_ASSIST: nx_int = 14 |
| 35 | const NX_PROOF_METHOD_VISUAL: nx_int = 15 // picture/diagram |
| 36 | const NX_PROOF_METHOD_TWO_COLUMN: nx_int = 16 // US-HS geometry form |
| 37 | const NX_PROOF_METHOD_ELEMENTARY: nx_int = 17 // restricted machinery |
| 38 | const NX_PROOF_METHOD_STATISTICAL: nx_int = 18 // pure-math statistical |
| 39 | const NX_PROOF_METHOD_AXIOM_CITATION: nx_int = 19 // single-axiom appeal |
| 65 | const NX_ATP_RESOLUTION: nx_int = 101 |
| 66 | const NX_ATP_MODEL_ELIMINATION: nx_int = 102 |
| 67 | const NX_ATP_TABLEAUX: nx_int = 103 |
| 68 | const NX_ATP_SUPERPOSITION: nx_int = 104 // + term rewriting |
| 69 | const NX_ATP_SAT_DPLL: nx_int = 105 |
| 70 | const NX_ATP_SMT_CDCL: nx_int = 106 |
| 71 | const NX_ATP_MODEL_CHECKING: nx_int = 107 |
| 72 | const NX_ATP_BDD: nx_int = 108 // binary decision diagram |
| 73 | const NX_ATP_HIGHER_ORDER_UNIF: nx_int = 109 |
| 74 | const NX_ATP_QUANTIFIER_ELIM: nx_int = 110 |
| 75 | const NX_ATP_TACTIC_LCF: nx_int = 111 // LCF tradition |
| 76 | const NX_ATP_PRESBURGER: nx_int = 112 // Presburger arithmetic decider |
functions
| 41 | func nx_proof_method_name(code: nx_int) -> *u8 called by 1: nx_method_report |
| 78 | func nx_atp_technique_name(code: nx_int) -> *u8 |
| 96 | func nx_proof_qed() -> *u8 { return "\xE2\x88\x8E" as *u8 } // ∎ called by 1: nx_method_report |
| 97 | func nx_proof_qed_text() -> *u8 { return "Q.E.D." as *u8 } |