Sequent bot demo site

---

Sequent bot is a sequent-style automated theorem prover for first-order predicate logic. For details, please refer to the GitHub repository.

The Misskey bot is also available!

You can find the user manual here.

Any bug reports or feedback are welcome. Please feel free to contact me on Twitter or Misskey.

Input some formula

---

Prove it!

Examples

---

• P ∨ ¬P
• ¬¬P → P
• P ∧ Q ↔ Q ∧ P
• P ∨ Q ↔ Q ∨ P
• ¬(P ∨ Q) ↔ (¬P ∧ ¬Q)
• ¬(P ∧ Q) ↔ (¬P ∨ ¬Q)
• ¬∀xP(x) ↔ ∃x¬P(x)
• ¬∃xP(x) ↔ ∀x¬P(x)
• ∃x∀yP(x,y) → ∀y∃xP(x,y)
• ∀x∃y(P(x) ∧ Q(y)) → ∃y∀x(P(x) ∧ Q(y))
• ∀x,y,zP(x,y,z) → ∀z,y,xP(x,y,z)
• P(a), ∀x(P(x) → P(f(x))) ⊢ P(f(f(f(a))))
• P(a), ∀x(P(x) → P(f(x))) ⊢ P(f(f(f(f(f(f(f(f(f(f(a)))))))))))