clayrat/sequent-calc

Experiments with sequent calculi

Language: Idris - Size: 281 KB - Last synced at: about 2 months ago - Pushed at: about 4 years ago - Stars: 27 - Forks: 3

wasabi315/LkProver

Language: OCaml - Size: 200 KB - Last synced at: 22 days ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

FlorianCassayre/master-project

Master Thesis Project at LARA (EPFL)

Language: Scala - Size: 940 KB - Last synced at: 3 days ago - Pushed at: almost 3 years ago - Stars: 3 - Forks: 0

FormalizedFormalLogic/LabelledSystem

Label-based Caliculi for Modal Logic

Language: Lean - Size: 43.9 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

DigammaF/kokonoe

Implementation of Gentzen's Sequent Calculus (LK) applied to creating and interrogating a database in natural language

Language: Python - Size: 21.5 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

clayrat/sequent-calc-talk

Code for the "Logic, machines and sequent calculus" talk

Language: Idris - Size: 11.7 KB - Last synced at: about 2 months ago - Pushed at: over 2 years ago - Stars: 31 - Forks: 0

boramalper/boolexman 📦

boolean expression manipulator for educational purposes

Language: JavaScript - Size: 961 KB - Last synced at: about 1 year ago - Pushed at: almost 6 years ago - Stars: 6 - Forks: 1

livrelogique/pravda

Pravda is a tool for teaching formal logic.

Language: TypeScript - Size: 174 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 7 - Forks: 2

joom/WangsAlgorithm

A classical propositional theorem prover in Haskell, using Wang's Algorithm.

Language: Haskell - Size: 17.6 KB - Last synced at: about 1 month ago - Pushed at: almost 6 years ago - Stars: 36 - Forks: 4

TypicalMath/stl

The Logic of Spacetime in Coq

Language: Coq - Size: 7.81 KB - Last synced at: 3 months ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

mizukami234/sequence-calculus-ruby

命題論理のシークエント計算の簡単な実装 (Ruby版)

Language: Ruby - Size: 1.95 KB - Last synced at: over 1 year ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 0

ayberkt/sequents

Proof search for intuitionistic propositional logic using Dyckhoff's LJT.

Language: Standard ML - Size: 311 KB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 26 - Forks: 0

jangjunha/elementary-logic-validator

형식언어 ℒ에서 Gentzen의 추론 규칙에 따른 논증 타당성 검증기

Language: Rust - Size: 118 KB - Last synced at: 6 days ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

proof-tree-builder/proof-tree-builder.github.io

A web-based graphical proof assistant for LK and Hoare logic.

Language: JavaScript - Size: 5.39 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 24 - Forks: 2

BelegCuthalion/stl

∇⎕ coloring

Language: TeX - Size: 249 KB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

artemmavrin/autoproof

Intuitionistic and classical propositional logic library

Language: Haskell - Size: 5.3 MB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 0

lucch/pesca

pesca: Proof Editor for Sequent Calculus

Language: Haskell - Size: 39.1 KB - Last synced at: about 2 years ago - Pushed at: over 8 years ago - Stars: 9 - Forks: 1

Champitoad/focalisation-classical-realizability

Présentation de l'article Focalisation and Classical Realizability de Guillaume Munch-Maccagnoni.

Language: TeX - Size: 350 KB - Last synced at: over 2 years ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0

ltics/tppa

a tiny LCF-style proof assistant.

Language: Haskell - Size: 19.5 KB - Last synced at: 5 months ago - Pushed at: almost 9 years ago - Stars: 1 - Forks: 0

ltics/sequent.idr

Language: Idris - Size: 1.95 KB - Last synced at: 5 months ago - Pushed at: over 8 years ago - Stars: 0 - Forks: 0

lxndrcx/proofTheoryHOL

Equivalence of natural deduction and sequent calculus in HOL4

Language: Standard ML - Size: 608 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0