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.

moduledescriptionlinesfuncs
nx_tptp.nxTPTP (Thousands of Problems for Theorem Provers) format2539
nx_tptp_emit.nxTPTP CNF emitter.2069
nx_tptp_emit_test.nxemitter smoke + parser round-trip.1574
nx_tptp_formula.nxTPTP CNF formula body parser.1582
nx_tptp_formula_test.nxTPTP CNF parser smoke + end-to-end2002
nx_tptp_load.nxend-to-end TPTP CNF file loader.2104
nx_tptp_load_any.nxTPTP loader handling both cnf(...) and fof(...).2072
nx_tptp_load_test.nxend-to-end smoke: load real TPTP files732
nx_tptp_symtab.nxTPTP identifier -> integer id table.1207
nx_tptp_term.nxTPTP term grammar -> *Term constructor.1423
nx_tptp_test.nxsmoke for the TPTP foundation reader.551
nx_tptp_write_test.nxwrite a clause set to disk, read it back,871