Logic Formalization Web

A web platform for logic courses where students formalize natural-language reasoning into propositional or first-order logic, and teachers review and grade submissions. Features automated validity checking via Z3 SMT solver and an LLM Challenge module for evaluating reasoning robustness of large language models.

Project Origin

The conceptualization of Logic Formalization Web originated from the research needs of Zhang Ming's team regarding LLM logic capability benchmarking. The core ideas and platform architecture were collectively envisioned by Zhang Ming, Yang Ruizhi,Peng Qiyuan, Shen Yujiong, Tan Kexin, Yu Zikang, and Gao Chichuan (in no particular order).

Features

For Students

• Formalization workspace — translate natural-language arguments into formal logic (propositional & first-order)
• LaTeX support — input and normalize logic formulas with live preview (KaTeX rendering)
• Automated validity checking — verify argument validity via Z3 SMT solver with counterexample display
• LLM Challenge — submit share links from LLM chatbots to demonstrate successful reasoning deception
• Review feedback — view teacher comments, grades, and verification results
• Soft-delete — delete submissions with confirmation dialog and JSON export (moved to recycle bin)

For Teachers

• Review panel — browse all student submissions with search, filter, and sort
• Content editing — modify student formulas directly with inline LaTeX editing
• Grading system — multi-level grades (Excellent / Good / Fair / Fail / Pending)
• Review history — automatic archival of past reviews with content snapshots
• LLM Challenge verification — verify each student LLM link with Pass/Fail status
• JSON export — export submission data for analysis
• Soft-delete — delete any submission with confirmation dialog and JSON export

For Administrators

• User management — batch create, delete, enable/disable users
• Role assignment — student, teacher, admin roles
• Password management — reset passwords with random generation
• Recycle bin — view, batch restore, or permanently delete soft-deleted submissions

Platform

• Bilingual UI — English / Chinese (中文) with one-click switch
• Guest Access — sandbox mode for anonymous users with ephemeral data
• Customizable header & footer — header subtitle text/link and ICP filing via .env
• JWT authentication — secure token-based auth with role-based access control
• Single-port Docker — one unified image, one port (3000), internal Nginx routing
• Subpath routing — deploy behind Nginx reverse proxy at any path

Tech Stack

Component	Technology
Frontend	Next.js 14, React 18, TypeScript, TailwindCSS, KaTeX
Backend	Python, FastAPI, SQLAlchemy (async), Pydantic v2
Database	PostgreSQL 15 with JSONB
Logic Engine	Z3 SMT Solver, lark parser
Auth	JWT (python-jose), bcrypt
Deployment	Docker, Nginx, supervisord

Quick Start

Prerequisites

• Docker & Docker Compose

1. Clone and configure

git clone https://github.com/ganganray/Logic-Translation.git
cd Logic-Translation
cp .env.example .env

Edit .env to set required values:

SECRET_KEY=<generate-a-random-string>
POSTGRES_PASSWORD=<strong-database-password>
ADMIN_USERNAME=admin

# Optional: Customize header subtitle and link
# NEXT_PUBLIC_HEADER_TEXT=Mathematical Logic at Fudan
# NEXT_PUBLIC_HEADER_LINK=https://logic.fudan.edu.cn

# Optional: Display ICP filing in footer (leave empty to hide)
# NEXT_PUBLIC_ICP=沪ICP备XXXXXXX号

Generate a secret key:

python3 -c "import secrets; print(secrets.token_urlsafe(48))"

2. Build & start

docker build -t ganganray/logic-formalization-web:latest .
docker compose -f docker-compose.prod.yml up -d

3. Get initial admin password

docker logs logic_app 2>&1 | grep -A5 "INITIAL ADMIN"

4. Access the application

Open http://localhost:3000 in your browser.

• Frontend and API are both served from port 3000
• API endpoints are at /api/... (e.g., /api/auth/login)

Development Setup

For local development with hot-reloading:

docker compose up -d

• Frontend: http://localhost:3000
• Backend: http://localhost:8000
• API docs: http://localhost:8000/docs

Deployment behind Nginx

For subpath deployment (e.g., at /logictranslation), only one location block is needed:

location /logictranslation/ {
    rewrite ^/logictranslation/(.*) /$1 break;
    proxy_pass http://localhost:3000;
    proxy_set_header Host $host;
    proxy_set_header X-Real-IP $remote_addr;
    proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
    proxy_set_header X-Forwarded-Proto $scheme;
}

Set in .env:

NEXT_PUBLIC_API_URL=/logictranslation/api

CLI Administration

# Reset a user's password
docker exec logic_app python3 /app/backend/scripts/reset_password.py <username> <new_password>

# Database backup
docker exec logic_db pg_dump -U postgres logictranslation > backup_$(date +%Y%m%d).sql

# Database restore
cat backup.sql | docker exec -i logic_db psql -U postgres logictranslation

Project Structure

.
├── backend/
│   ├── app/              # FastAPI application
│   ├── alembic/           # Database migrations
│   ├── scripts/           # CLI tools (init_admin, reset_password)
│   └── requirements.txt
├── frontend/
│   └── src/
│       ├── app/           # Next.js pages
│       ├── components/    # Shared components
│       └── utils/         # Auth, i18n, API helpers
├── docker/                # Nginx, supervisord, entrypoint
├── wiki/                  # Documentation
├── Dockerfile             # Unified production image
├── docker-compose.yml     # Development
├── docker-compose.prod.yml # Production
└── .env.example           # Environment variable template

License

Apache License 2.0