coq-sequent-calculus
Logical Deduction Library
Formalizations of logical deduction systems using Coq
Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic
44 stars
6 watching
3 forks
Language: Coq
last commit: over 8 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
| coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
| coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 45 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 geocoq/geocoq | A formalization of geometry using the Coq proof assistant. | 186 |
| coq-community/math-classes | A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq | 162 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 math-comp/analysis | A comprehensive Coq proof-assistant library for mathematical analysis | 206 |