About & Documentation

Project Overview

🎓 FormalCS Platform

A full-stack web application implementing Three formal methods modules: Finite Automata Simulator, Resolution Method Solver, and NNF/CNF/DNF Transformer.

All computational logic is implemented in Python on a Flask backend. JavaScript is used exclusively for UI interactivity, visualization, and asynchronous requests to the API. The frontend uses Cytoscape.js for graph rendering of automata state diagrams.

Architecture

📐 Project Structure

ProofLab/
├── app.py
├── requirements.txt
├── algorithms/
│   ├── automata.py
│   ├── pda.py
│   ├── resolution.py
│   └── transformer.py
├── templates/
│   ├── base.html
│   ├── index.html
│   ├── automata.html
│   ├── resolution.html
│   ├── transformer.html
│   └── about.html
└── static/
    ├── css/
    │   ├── main.css
    └── js/
        │   ├──main.js

Module Documentation

Module 1 — Finite Automata Simulator

Simulates both DFA (Deterministic Finite Automaton) and NFA (Non-deterministic Finite Automaton) machines on input strings.

Python implementation: algorithms/automata.py — FiniteAutomaton class handles state transitions, ε-closure computation for NFA, acceptance checking, and step-by-step tracing. The get_graph_data() method returns nodes and edges for Cytoscape.js rendering.

Module 2 — Resolution Method Solver

Applies resolution to propositional logic formulas. Converts formula to CNF, extracts clauses, then iteratively applies resolution until empty clause (UNSAT) or saturation (SAT).

Python implementation: algorithms/resolution.py — full recursive-descent parser → AST transformations (eliminate_iff → eliminate_imp → push_negation → distribute_or) → clause extraction → resolution_solver().

⟺ Module 3 — Formula Transformer (NNF / CNF / DNF)

Transforms any propositional formula to NNF, CNF, and DNF with detailed step annotations. Also generates truth tables and classifies formulas as tautology, contradiction, or satisfiable.

Python implementation: algorithms/transformer.py uses the same AST system as resolution.py. to_nnf(), to_cnf(), to_dnf() use different distribution directions. compute_truth_table() evaluates over all 2ⁿ assignments.

API Reference

🔌 REST Endpoints

POST /api/automata/simulate Simulate FA on input string

POST /api/automata/graph Get graph data only

POST /api/resolution/solve Resolution method proof

POST /api/transformer/transform NNF / CNF / DNF + truth table

Technologies Used

Python 3.13+

All algorithms & backend logic

Core

Flask 3.1.3

Web framework & REST API

Backend

Jinja2

HTML templating with inheritance

Backend

Cytoscape.js

Automata graph visualization

Frontend

Vanilla JS

UI interactions & fetch API

Frontend

CSS Variables

Design system & theming

Frontend

About & Docs