Beweren en bewijzen/supplement/verbeterpunten (voor docenten)

Op deze pagina een lijstje van dingen die verbeterd (zouden) moeten worden in een volgend jaar.

Verbeterpunten 2013

• De uitleg over de systematische methode van het vertalen naar predikaatlogica. (David)
• Zoveel mogelijk stof omzetten naar LaTeX ivm boek. (Engelbert)

Verbeterpunten 2014

• De uitleg over het rationaliteitsvierkant. Kan er bij de kolom eigenschappen misschien beter worden gesproken over eigenschappen of functies? Meteen de naamgeving met de rationaliteitskubus aanpassen. (David, Engelbert, Hanno)
• Leertaak 5 gebruikt nu een plaatje met tautologieën, maar daarbij wordt ⊢ gebruikt terwijl op dit moment dat eigenlijk |= zou moeten zijn. Verder staan er geen stellingen bij met ↔. (Engelbert)
• Leertaak 9: overleden -> overlijdt; geboren -> wordtGeboren. Misschien expliciet types in de opgave aangeven.
• Natuurlijke deductie:
  • Naamgeving is in Coq net andersom: ∨1I of dis_i1. [Engelbert: deductieschema aangepast op 10/02/14]
  • Coq geeft eerst de bewijsverplichting met ¬α en dan pas die met α. Dit misschien aanpassen in het sjabloon. (Liever in Coq, maar dat kan ik in elk geval niet zelf.) [Engelbert: deductieschema aangepast op 10/02/14]
  • In plaats van een 'math' regel verschillende regels voor 'interval' etc. [Engelbert: deductieschema aangepast op 28/05/13]
  • Een officiele cursus in ProofWeb aanvragen zodat studenten zelf direct commentaar krijgen op hun gemaakte oefeningen.
• Onderscheid formele en informele bewijzen duidelijk(er) maken.
  • In het bijzonder bij leertaak 10 en 11 de vraag „Hoe kun je hem uitleggen in natuurlijke taal?” expliciet maken door informele bewijzen op te schrijven. Dit met de hoop dat studenten bij andere vakken makkelijker kunnen herkennen wanneer er een (rode) all_i of een (groene) exi_i wordt gedaan. David stelt hier een tandem-college voor: een docent geeft een bewijs met natuurlijke deductie en de andere bewijst hetzelfde in natuurlijke taal.
• Grammatica aanpassen zodat de in Coq niet toegestane notatie ∀x:(3,7] helemaal niet meer toegestaan is. Dan zijn de pas ingevoerde dom-regels ook niet meer nodig. [Engelbert: grammatica aangepast op 10/02/14]
• Het dossier-sjabloon wat aanpassen zodat duidelijk is wat men wanneer moet invullen. Het verhaal over de leerdoelen in het begin van de cursus, iets halverwege en een verslag aan het einde. Nu zijn er mensen die aan het eind gaan beschrijven wat ze van de leerdoelen vinden. Op zich ook niet erg, maar dat is niet de bedoeling. [Engelbert: sjabloon aangepast op 04/02/14]
• Duidelijke afspraken over het feit dat het niet de bedoeling is om 'geinige plaatjes' te uploaden. Indien er niet zelf voor een foto wordt gezorgd zal de foto uit Osiris worden gehaald. (Dit omdat sommige sjablonen niet helemaal lekker werken als er geen foto is.)
• Werkstuksjabloon aanpassen.
  • Rationaliteitsvierkant explicieter laten terugkeren.
  • Sommige dingen worden dubbel gedaan: eerst 'gewoon' in het werkstuk en daarna 'formeel' in Coq. Door die formele Coq-notatie al eerder te gebruiken, kunnen waarschijnlijk veel inconsistenties voorkomen worden.

Verbeterpunten 2015

• Werkstuksjabloon aanpassen: niet printen van bewijzen; kijken of er een tijdslijn gevraagd kan worden,...
• Rubric maken om beoordeling uniformer te krijgen.
• Voortaan blokken in plaats van lijnen gebruiken bij systematische vertaling.
• Bij de systematische vertaling even kijken waar de haakjes precies moeten staan bij de kwantorformules: (∀ t:T, blok) of ∀ t:T, (blok).
• Beoordelingen voor leertaken moeten beter aangeven of de uitwerking goed was en niet alleen maar of er sprake was van vlijt.
• Grammatica controleren: voorbeeld disjunctie/conjunctie op verkeerde plek?
• Meer opgaven bedenken voor Coq (met name in 'Getallen').
• Meer aandacht voor concrete uitleg over handigheidjes in Coq, zoals eindige verzamelingen, lemma's etc.
• Grote Coq-bewijzen leveren problemen op in de werkplaats, waardoor het hele werkstuk niet meer te zien is. Sjabloon aanpassen om het werkstuk op te slaan onder een van de useraccounts voor Coq. Heeft als nadeel dat de historie handmatig moet worden verzorgd.
• Opgave predikaatlogica_064 is niet volledig. Het moet zijn:

  Theorem exercise_064 : exists x1 : D, exists x2 : D, P x1 \/ P x2.

Verbeterpunten 2016

• Verschillende taken moeten de producten exacter worden weergegeven.
• Taak 4:
  • Explcieter maken dat er metingen moeten worden opgegeven.
• Taak 5:
  • Kopieer de onderdeeldefinities van de vorige taak.
  • Indien de stelling of de onderdelen versimpeld zijn, moeten die er expliciet staan.
• Taak 6:
  • Expliciet vragen om eerste vermoedens.
  • Expliciet vragen om tegenvoorbeelden.
  • Basispredikaat 'Past' moet naar hulpdefinities.