]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6f64f2b) | patch
A very nice experiment using notation: we define the notation for natural
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 11 Jul 2008 17:22:19 +0000 (17:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 11 Jul 2008 17:22:19 +0000 (17:22 +0000)
commit7ce9eb0e973e414c988b416d118efe860516e275
tree896b0384e73081d3ebd5203d04d8942d33850a95tree | snapshot
parent6f64f2bbba6d5488cc36b8e2f5a717e866a3015dcommit | diff
A very nice experiment using notation: we define the notation for natural
language derivations so that, when looking at the proof, we see it as a
natural deduction tree! Useful to teach logic to first year students, but
much work still need to be done (expecially to give derivation trees to
the system in some way).
helm/software/matita/library/demo/natural_deduction.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.