English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We have developed an alternative approach to teaching computer sciencestudents how to prove. First, students are taught how to prove theorems withthe Coq proof assistant. In a second, more difficult, step students willtransfer their acquired skills to the area of textbook proofs. In this articlewe present a realisation of the second step.  Proofs in Coq have a high degree of formality while textbook proofs have onlya medium one. Therefore our key idea is to reduce the degree of formality fromthe level of Coq to textbook proofs in several small steps. For that purpose weintroduce three proof styles between Coq and textbook proofs, called line byline comments, weakened line by line comments, and structure faithful proofs.  While this article is mostly conceptional we also report on experiences withputting our approach into practise.

Learning how to Prove: From the Coq Proof Assistant to Textbook Style