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.

Microservices Docker Images: https://hub.docker.com/u/kevdev0247
(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 ) )