TypicalMath

205 Yassemi Dead End, UT

Pinned Repositories

cpc
A try to implement the completeness theorem of classical propositional logic
Language:Coq0 1 02
hilbert-gentzen
Every Hilbert-style proof has a Natural couterpart, and vice versa.
Language:Coq0 1 01
lambda2
An implementatino of λ2 system, with some simple properties
Language:Coq0 1 00
nat-finset
Re-inventing finite sets (because (learning) ssreflect is overkill)
Language:Coq0 1 00
prop-calc
Propositional Calculus in Coq by Floris van Doorn
Language:Coq3 1 00
ruitenburg1984
A https://git8.cs.fau.de/software/ruitenburg1984/ fork
Language:Coq00
stl
The Logic of Spacetime in Coq
Language:Coq00
subst-interpol
Uniform Interpolation for some Substructural Logics (work in progress)
Language:Coq2 2 00

TypicalMath's Repositories

TypicalMath/prop-calc
Propositional Calculus in Coq by Floris van Doorn
Language:Coq3 1 00
TypicalMath/subst-interpol
Uniform Interpolation for some Substructural Logics (work in progress)
Language:Coq2 2 00
TypicalMath/cpc
A try to implement the completeness theorem of classical propositional logic
Language:Coq0 1 02
TypicalMath/hilbert-gentzen
Every Hilbert-style proof has a Natural couterpart, and vice versa.
Language:Coq0 1 01
TypicalMath/lambda2
An implementatino of λ2 system, with some simple properties
Language:Coq0 1 00
TypicalMath/nat-finset
Re-inventing finite sets (because (learning) ssreflect is overkill)
Language:Coq0 1 00
TypicalMath/ruitenburg1984
A https://git8.cs.fau.de/software/ruitenburg1984/ fork
Language:Coq00
TypicalMath/stl
The Logic of Spacetime in Coq
Language:Coq00