A web-based graphical proof assistant for LK and Hoare logic.
-
Updated
Jan 10, 2026 - JavaScript
A web-based graphical proof assistant for LK and Hoare logic.
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
Code for the "Logic, machines and sequent calculus" talk
Proof search for intuitionistic propositional logic using Dyckhoff's LJT.
pesca: Proof Editor for Sequent Calculus (mirror)
Pravda is a tool for teaching formal logic.
boolean expression manipulator for educational purposes
Lean 4 Mechanization about Provability Logics
Master Thesis Project at LARA (EPFL)
형식언어 ℒ에서 Gentzen의 추론 규칙에 따른 논증 타당성 검증기
A Lean 4 formal lab that mathematically guarantees the structural boundaries for NF Set Theory.
A webapp for creating sequent proof of propositional formulas
Equivalence of natural deduction and sequent calculus in HOL4
Intuitionistic and classical propositional logic library
Présentation de l'article Focalisation and Classical Realizability de Guillaume Munch-Maccagnoni.
Label-based Caliculi for Modal Logic
Coq implementation of a Gentzen G' propositional sequent prover
To associate your repository with the sequent-calculus topic, visit your repo's landing page and select "manage topics."