Module fol_model 

FOL → runnable Rust model-checker / temporal monitor.

Compiles a first-order (optionally temporal) formula into a self-contained, reusable Rust module: a World you populate with individuals + facts, and a holds(...) that evaluates the rule against it — so a rule/invariant can be encoded once and used against your own state.

• Quantifiers: ∀→.all, ∃→.any over World::domain.
• Predicates: table lookups (World::pred).
• Events (Neo-Davidsonian, e.g. “read”): ∃e. read(e) ∧ Agent(e,x) ∧ Theme(e,y) → an existential over the domain treating events as first-class entities.
• Temporal (always/eventually/next/until): a finite-trace monitor over &[World] (Always→all states, Eventually→any, …) plus an incremental Monitor. Pure O(trace) evaluation — no SMT, no std::time, no randomness, WASM-safe. (The native automaton path is logicaffeine_verify::automata, which carries a Z3 crate dep; this mirrors its semantics WASM-safely.)

Functions

fol_to_model_checker

Emit a self-contained Rust rule module for premises ⊨ goal (empty premises = check the single formula goal). english/fol are echoed as doc comments.

fol_to_model_checker_module

Like fol_to_model_checker, but emits NO demo fn main — the form bundled into an imperative program’s mod proven (which has its own main). Produces only the World + holds (+ Monitor) library items.