Learning how to Prove: From the Coq Proof Assistant to Textbook Style
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...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2018-03-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1803.01466v1 |
id |
doaj-78239f88c2cf4523a980ea3d9e66e666 |
---|---|
record_format |
Article |
spelling |
doaj-78239f88c2cf4523a980ea3d9e66e6662020-11-25T02:18:59ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-03-01267Proc. ThEdu 201711810.4204/EPTCS.267.1:11Learning how to Prove: From the Coq Proof Assistant to Textbook StyleSebastian Böhne0Christoph Kreitz1 Universität Potsdam Universität Potsdam 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.http://arxiv.org/pdf/1803.01466v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Sebastian Böhne Christoph Kreitz |
spellingShingle |
Sebastian Böhne Christoph Kreitz Learning how to Prove: From the Coq Proof Assistant to Textbook Style Electronic Proceedings in Theoretical Computer Science |
author_facet |
Sebastian Böhne Christoph Kreitz |
author_sort |
Sebastian Böhne |
title |
Learning how to Prove: From the Coq Proof Assistant to Textbook Style |
title_short |
Learning how to Prove: From the Coq Proof Assistant to Textbook Style |
title_full |
Learning how to Prove: From the Coq Proof Assistant to Textbook Style |
title_fullStr |
Learning how to Prove: From the Coq Proof Assistant to Textbook Style |
title_full_unstemmed |
Learning how to Prove: From the Coq Proof Assistant to Textbook Style |
title_sort |
learning how to prove: from the coq proof assistant to textbook style |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2018-03-01 |
description |
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. |
url |
http://arxiv.org/pdf/1803.01466v1 |
work_keys_str_mv |
AT sebastianbohne learninghowtoprovefromthecoqproofassistanttotextbookstyle AT christophkreitz learninghowtoprovefromthecoqproofassistanttotextbookstyle |
_version_ |
1724879405707165696 |