theorem-prover-kt

Description

A sequent-style theorem prover for first-order logic implemented in Kotlin.

Rust rewrite

I am rewriting this project in Rust. See theorem-prover-rs.

Demo site

Misskey bot

@[email protected]

Twitter bot

@sequent_bot

How to use

git clone https://github.com/boitsov14/theorem-prover-kt.git
cd theorem-prover-kt
chmod +x gradlew
./gradlew shadowJar
java -jar build/libs/theorem-prover-kt-all.jar "∃x∀yP(x,y) → ∀y∃xP(x,y)"
latex out.tex
dvipng out.dvi

APIs

api-for-theorem-prover

Special Thanks

• Build Your Own First-Order Prover
• stepchowfun/theorem-prover
• qnighy/ipc_solver