A complete toolkit for automata simulation, logic resolution, and formula transformation — all powered by a Python backend.
Every module runs its algorithms entirely on the Python backend — the frontend only renders results. Five more modules are in the pipeline.
Switch between DFA, NFA, and PDA with a single click. The Python backend handles all transition logic — ε-closures, stack operations, configuration BFS — and returns the full execution trace.
Enter any propositional formula. The solver automatically converts it to CNF, extracts the clause set, and applies resolution until it derives the empty clause (UNSAT) or saturates (SAT).
Three normal forms computed simultaneously from a single formula input, each with annotated transformation steps and the applicable equivalence law shown at every stage.
Pure Python for every algorithm. JavaScript only for rendering.
The platform is actively growing. These modules are designed, scoped, and queued for development — each extending the formal-methods toolkit further.
First-order unification via Robinson's Algorithm — already referenced in the tech stack. Input two terms; the solver computes the most general unifier (MGU) step-by-step, showing each substitution applied and the resulting unified term.
Context-Free Grammar designer and analyzer. Define productions in BNF notation, then derive strings step-by-step — both leftmost and rightmost. Detects ambiguity, computes FIRST/FOLLOW sets, and optionally converts to Chomsky Normal Form.
Analytic tableau method for propositional and first-order logic. Constructs the branching proof tree automatically, closes branches on contradictions, and classifies formulas as tautology, satisfiable, or unsatisfiable.
Visual Turing Machine simulator with tape rendering. Define states, alphabet, and transition function; watch the read/write head move step-by-step across the tape. Supports multi-step execution and halting detection.
Beyond new modules, these cross-cutting improvements will enhance the platform experience across every tool.
Jump straight into the platform. No setup required — everything runs locally with a single command.