code wiki / tptp
topic: tptp
12 modules sharing the tptp name family (derived from the tree's prefix discipline).
The 'tptp' topic family provides tools for working with the TPTP format within the Nishi sovereign ecosystem, enabling the parsing, emission, and loading of TPTP CNF formulas. The nx_tptp module defines the TPTP format structure, while nx_tptp_emit generates CNF formulas for theorem proving tasks. nx_tptp_load_any supports loading both CNF and FOF formulas from TPTP files, ensuring compatibility and flexibility in handling different problem representations.
auto-narrated by the local model from this topic's module headers; links verified against the wiki index.
narrated overview -- maintained by the narration lane, module links verified against this wiki.
| module | description | lines | funcs |
|---|---|---|---|
| nx_tptp.nx | TPTP (Thousands of Problems for Theorem Provers) format | 253 | 9 |
| nx_tptp_emit.nx | TPTP CNF emitter. | 206 | 9 |
| nx_tptp_emit_test.nx | emitter smoke + parser round-trip. | 157 | 4 |
| nx_tptp_formula.nx | TPTP CNF formula body parser. | 158 | 2 |
| nx_tptp_formula_test.nx | TPTP CNF parser smoke + end-to-end | 200 | 2 |
| nx_tptp_load.nx | end-to-end TPTP CNF file loader. | 210 | 4 |
| nx_tptp_load_any.nx | TPTP loader handling both cnf(...) and fof(...). | 207 | 2 |
| nx_tptp_load_test.nx | end-to-end smoke: load real TPTP files | 73 | 2 |
| nx_tptp_symtab.nx | TPTP identifier -> integer id table. | 120 | 7 |
| nx_tptp_term.nx | TPTP term grammar -> *Term constructor. | 142 | 3 |
| nx_tptp_test.nx | smoke for the TPTP foundation reader. | 55 | 1 |
| nx_tptp_write_test.nx | write a clause set to disk, read it back, | 87 | 1 |