Proofster

A proof assistant platform automating preprocessing and normalization procedure before resolution proofs in the context of first order logic, drastically reduce human errors of doing calculation by hand.

(GKE Deployment no longer active! currently migrating from GKE Autopilot to Regular Cluster to save cost)

See the bottom section Gallery for UI/UX

Tech stack

Frontend: Typescript (React, Redux Toolkit, Axios, MaterialUI, HTML, CSS)

Microservices: Python (Django, PostgreSQL), Go (Gin, Goroutine, MongoDB), RabbitMQ, Docker, Kubernetes, GCP

Domain Layer: Vanilla Python (Recursive Algorithms, Binary Trees), AWS (Lambda, API Gateway)

System Design

Data Structure (Sample Data Structure and UML Diagram)

Algorithm Execution Workflow (Sequence Diagram)

Lifecycle of a Formula (Sequence Diagram)

Gallery

Editor & Control Panel

Steps generation

Stages propagation reaches end

Stats and dashboard

Mobile Responsive Features

Getting Started

Algorithm Service

Run

go run main.go

Inside ~/Projects/proofster/microservices/algorithm

Workspaces Service

Run

poetry run python manage.py runserver 0.0.0.0:8001

Inside ~/Projects/proofster/microservices/workspaces

Formulas Service

Run

poetry run python manage.py runserver 0.0.0.0:8002

Inside ~/Projects/proofster/microservices/formulas

Frontend

Run

npm start 

Inside ~/Projects/proofster/frontend

Trying it Out

Infix

 ∀x  ∃y  (  (  F(y)  ∧  G(y)  )  ∨  ¬  (  F(x)  ⇒  G(x)  )  )
 ∀x  (  F(x)  ⇒  ¬  (  H(x)  )  )
 ∀x  (  F(x)  ⇒  ¬  (  G(x)  )  )
 ∀x  (  ¬  (  F(x)  )  )

Postfix

input FORM F y FORM G y AND FORM F x FORM G x -> OR EXIST y FORALL x
input FORM F x FORM H x NOT -> FORALL x
input FORM F x FORM G x NOT -> FORALL x
input FORM F x NOT FORALL x

Natural

FORALL x EXIST y ( ( FORM F y AND FORM G y ) OR NOT ( FORM F x -> FORM G x ) )
FORALL x ( FORM F x -> NOT ( FORM H x ) )
FORALL x ( FORM F x -> NOT ( FORM G x ) )
FORALL x ( NOT ( FORM F x ) )