Logicaffeine Documentation

API documentation for the Logicaffeine workspace — the LOGOS English programming language, its logic pipeline, proof engines, execution tiers, and platform crates.

AI agents: start at llms.txt — a plain-text map of every crate, module and item, with one file per crate.

Start here

Logic: English in, first-order logic out

• Turn an English sentence into first-order logic — The one-call entry point, default options; the `compile_*` functions beside it add output formats, discourse, ambiguity and scope.
• Get every quantifier-scope reading of a sentence — One formula per scope permutation when a sentence has several quantifiers.
• Get every parse of an ambiguous sentence — All valid readings, lexical (noun/verb) and structural.
• Carry pronouns and tense across sentences — Compiles a discourse, tracking temporal order; `compile_with_discourse` shares state across calls.
• Lower modal operators to possible worlds — Kripke semantics: necessity and possibility become explicit quantification over worlds.
• Add conversational implicatures — Scalar implicature enrichment on top of the literal reading.
• Render a formula in another notation — The output formatters for logical expressions.
• Parse English into a syntax tree — The recursive-descent parser for natural language; the tree it builds is in `ast`.
• Resolve anaphora and scope — Discourse Representation Structures.
• Look up how a word behaves — The lexicon's grammatical and semantic categories: verb classes, transitivity, animacy, gender, number.

Proof: every theorem checked by a small kernel

• Prove a goal from premises and get a kernel-checked proof — Backward-chaining search, certification into a kernel term, and a kernel type-check in one call.
• Prove a theorem written in English — Compiles and proves a theorem block.
• Find out whether premises contradict each other — Returns a kernel-checked proof of False and the clashing premises.
• Prove a library of theorems in citation order — Each theorem proved from its premises plus the conclusions it cites.
• Type-check a term in the Calculus of Constructions — The kernel itself: `Term`, `Context`, `normalize` and the universe hierarchy sit beside it.
• Talk to the kernel in its vernacular — The command language, its term parser and the REPL.
• Re-check a proof term independently — A second checker, the de Bruijn criterion taken seriously; re-checkable certificates are in `certificate`.
• Decide ring equalities — Polynomial equality by normalization.
• Decide integer arithmetic — The Omega test; Fourier–Motzkin linear arithmetic is in `lia`.
• Simplify and close goals by rewriting — The simplifier tactic; congruence closure is in `cc`.
• Prove interactively with tactics — A tactic framework with a first-class goal state.
• Write a proof as a script — Proofs as text over the tactic combinators, the way a Lean or Coq proof reads.
• Search a named lemma library — `exact?`, `apply?` and premise selection over certified lemmas.
• Get a counterexample when a goal is false — Exhibits a model instead of failing silently.
• Read formal first-order logic text — A parser from formal FOL surface syntax into the prover's expressions.

Solving: SAT and certified refutations

• Decide a CNF formula — Routes through every cheap specialist before CDCL; `solve_comprehensive` runs the full arsenal.
• Use the CDCL SAT core directly — Conflict-driven clause learning.
• Read and write DIMACS CNF — The SAT-competition interchange format.
• Emit a refutation other checkers accept — DRAT, LRAT and DPR traces.
• Check a refutation — Reverse unit propagation; propagation-redundancy checking is in `pr`.
• Break symmetry, with a certificate — Lex-leader symmetry-breaking predicates that come with a proof.
• Count models, weighted and up to symmetry — The partition function, one solve per model orbit.
• Reason with cardinality and pseudo-Boolean constraints — Cutting planes, a proof system stronger than resolution.
• Reason about parity — XOR-SAT by Gaussian elimination over GF(2).
• Model-check without Z3 — Bounded model checking, k-induction and vacuity, certified and browser-ready.

Mathematics: exact, and certified where it counts

• Solve linear systems exactly over the rationals — Exact linear algebra over ℚ.
• Turn an exact solve into a kernel-checked proof — Kernel-certified linear algebra.
• Do linear algebra modulo a prime or a composite — GF(p); composite moduli by the Chinese Remainder Theorem are in `modm`.
• Refute with polynomials — Polynomial calculus and the Nullstellensatz over GF(2); other fields and rings are in `polycalc_gfp` and `polycalc_zm`.
• Refute with sums of squares — Positivstellensatz refutations over ℚ, kept exact.
• Reduce a lattice — LLL lattice reduction.
• Compute on elliptic curves — Elliptic-curve primitives over ℤ/N.
• Walk isogeny graphs — Certified isogeny torsion-image witnesses; 𝔽_{p²} arithmetic and the supersingular graph are in `fp2`.
• Work with permutation groups — Schreier–Sims: a base and strong generating set.
• Hold a homotopy type as an object — Eilenberg–MacLane spaces K(A, n); Kan complexes are in `kan_complex`.
• Attack a multivariate quadratic system — XL algebraic cryptanalysis by linearization.
• Compute with arbitrary-precision integers — The numeric tower's foundation.
• Carry physical units through a computation — Exact magnitudes with a physical dimension and a unit.
• Count money exactly — An exact amount in a specific currency; exact calendar time is in `temporal`.
• Compute in finite fields and wrapping rings — GF(2⁸); the wrapping integer rings ℤ/2ᵏ are in `word`.

Verification: specifications against implementations

• Prove two programs or specifications equivalent — Z3-backed semantic equivalence; the verify crate needs Z3 and a Pro-or-higher license.
• Prove unbounded safety — IC3/PDR; k-induction and interpolation are in `kinduction` and `interpolation`.
• Synthesize a controller from temporal logic — Reactive synthesis from LTL.
• Prove the compiled Rust matches the LOGOS source — SMT translation validation.
• Turn English hardware specs into assertions — SVA and PSL generation for hardware verification.

Programs: running English code

• Compile a LOGOS program — The compilation pipeline.
• Run a program on the tree-walking interpreter — The tree-walking interpreter for imperative LOGOS.
• Run a program on the bytecode VM — The register VM the JIT tiers up from.
• Generate Rust from LOGOS — Code generation from the LOGOS AST to Rust source.
• Extract a program from a proof — Program extraction from kernel terms to Rust.
• Run concurrent programs deterministically — The scheduler, channels, seeds and choice traces behind reproducible concurrency.
• Replicate data without conflicts — Conflict-free replicated data types.
• Reach files, storage and the network — Platform IO, persistence, HTTP and post-quantum crypto kernels.
• Drive the toolchain from the command line — largo: new, build, run, check, verify, publish.
• Serve LOGOS to an editor — The language server.

Crates

• logicaffeine_language — The LOGOS front end: English sentences to first-order logic, and the parser for LOGOS programs and LGX pages · map
• logicaffeine_compile — The LOGOS compiler: type checking, the optimizer, the interpreter and bytecode VM, and the Rust, C, WASM, RISC-V, CUDA and hardware backends · map
• logicaffeine_proof — Kernel-checked proof search and tactics, certified SAT/CDCL with DRAT/LRAT output, and a number-theory and cryptanalysis library · map
• logicaffeine_kernel — Calculus of Constructions proof kernel with inductive types, universes, quotients, a second checker and Lean 4 import · map
• logicaffeine_verify — Z3-based static verification and model checking for Logicaffeine · map
• logicaffeine_tv — Translation validation for LOGOS: a symbolic encoder of the source, checked with Z3 against the tree-walking interpreter per program · map
• logicaffeine_lexicon — The English vocabulary behind LOGOS: verb, noun and adjective metadata for build-time lookup tables, plus an optional runtime JSON index · map
• logicaffeine_base — Foundation types for Logicaffeine: arenas, string interning, spans, and exact integers, decimals, quantities, money, dates and UUIDs · map
• logicaffeine_data — LOGOS runtime values, collections, wire format and CRDTs, shared by native and WASM builds · map
• logicaffeine_system — Platform IO, networking, HTTP serving, persistence, and post-quantum crypto (Keccak/SHA-3, ChaCha20-Poly1305, ML-KEM, ML-DSA) for LOGOS · map
• logicaffeine_runtime — Deterministic, replayable concurrency runtime for the LOGOS interpreter and VM: task scheduler, channels, Select, timers, seed and trace · map
• logicaffeine_forge — The machine-code layer of the LOGOS copy-and-patch JIT: W^X executable memory, build-time stencils, a register-allocating x86-64 backend · map
• logicaffeine_jit — Native execution tier for the LOGOS bytecode VM: hot functions and loops tier up to x86-64 machine code · map
• logicaffeine_lsp — The LOGOS language server (LSP): diagnostics, completion, hover, navigation and refactoring for .lg files, literate .md files and LGX pages · map
• logicaffeine_cli — largo — the LOGOS build tool: projects, builds, tests, serving, proofs, and the package registry · map
• logicaffeine_web — The logicaffeine.com site (Dioxus/WASM): LOGOS Studio with live LGX previews, Learn, Syntax Guide, benchmarks, news and the registry browser · map