Announcement. A introductory tutorial on natural deduction in Coq Natürliches Schließen in Coq, written in German is available at https://esb-dev.github.io/mat/nsc.pdf. The tutorial introduces natural deduction according to Gerhard Gentzen and then shows how to do natural deduction in Coq. It is intended as a simple, first introduction to natural deduction and as a first acquaintance with Coq.
Comments welcome.
Burt.
Hi Burt,
I am not a German speaker myself, but I can only applaud such initiatives. It is always a good thing to produce more introductory material in various languages, so that people who are not comfortable with English can still learn about Coq.
You may be aware of our effort to create language-specific categories in this forum, so that people who are not comfortable with English can still come and ask questions. In particular, there is a category for German: https://coq.discourse.group/c/coq-in-german.
These categories have not been a success so far, probably because the target audience is not aware of their existence. May I suggest that you mention the existence of this German sub-forum in your tutorial?
Conversely, you could cross-post this announcement in German in https://coq.discourse.group/c/coq-in-german/coq-in-german-announcements. As of today, it won’t really help to reach out to more people, but in the long-term, it might make your tutorial easier to discover for people looking specifically for German resources.