issues
search
elexunix
/
qock
This project is currently an implementation of a proof-checker. But it is planned to be extended; for example, to support algorithm extraction from intuitionistic proofs, which is considered to be an interesting feature.
0
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
We may write a template mechanism for automated proving of tautologies
#8
elexunix
opened
3 years ago
0
Too verbose syntax
#7
MikailBag
opened
3 years ago
0
It's time to write the first proof
#6
elexunix
closed
3 years ago
1
Maybe propositional axioms might better be updated to check well-formation?
#5
elexunix
opened
3 years ago
2
Add zfc axiom system file
#4
elexunix
opened
3 years ago
1
Its time to start making a template proof library
#3
elexunix
opened
3 years ago
0
[Major goal] Intuitionistic proofs to algorithms effectively
#2
elexunix
opened
3 years ago
1
is_wff probably doesn't work properly
#1
elexunix
opened
3 years ago
0