TY  - GEN
A1  - Böhne, Sebastian
A1  - Kreitz, Christoph
T1  - Learning how to prove
T2  - Electronic proceedings in theoretical computer science
N2  - We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their acquired skills to the area of textbook proofs. In this article we present a realisation of the second step. Proofs in Coq have a high degree of formality while textbook proofs have only a medium one. Therefore our key idea is to reduce the degree of formality from the level of Coq to textbook proofs in several small steps. For that purpose we introduce three proof styles between Coq and textbook proofs, called line by line comments, weakened line by line comments, and structure faithful proofs. While this article is mostly conceptional we also report on experiences with putting our approach into practise.
Y1  - 2018
UR  - https://publishup.uni-potsdam.de/frontdoor/index/index/docId/54078
SN  - 2075-2180
IS  - 267
SP  - 1
EP  - 18
PB  - Open Publishing Association
CY  - Sydney
ER  -