Korte beschrijving van het onderwijsinnovatieproject

Samenvattend

Het project heeft tot doel om nieuwe modules te ontwikkelen voor een bestaande webtoepassing voor zelfstudie zodat ze kan gebruikt worden in de logica-gerelateerde vakken uit de faculteit Wetenschappen, meer bepaald de vakken Redeneren, Abstraheren en Formuleren en Logisch programmeren uit de opleiding Informatica en Discrete Wiskunde 1 (onderdeel logica) en Logica uit de opleiding Wiskunde.

Bestaande webtoepassing

De faculteit Letteren en Wijsbegeerte gebruikt reeds meer dan 20 jaar het zogenaamde logica- programma van collega Diederik Baetens als oefenprogramma voor logicavakken in diverse opleidingen (waar dit programma de begeleide oefeningensessies grotendeels vervangt). Doorheen de jaren is het programma geëvolueerd van een opdrachtlijnprogramma onder MS-DOS naar een programma met grafische gebruikersinterface onder Windows (nog steeds te vinden op Athena onder de naam Logica) tot het vorig jaar is omgezet naar een online webtoepassing binnen het Alice-platform van onze universiteit. (Uitproberen kan op alicelw.ugent.be, ev. als anonieme gebruiker.)

De nieuwe webtoepassing bevat opgaven uit verschillende domeinen van de logica (propositielogica, predicatenlogica, modale logica, redeneren in natuurlijke taal, …) en ondersteunt heel wat verschillende vragentypes, van eenvoudige waar/vals-vragen en invuloefeningen, over oefeningen waarbij men een Nederlandse zin moet omzetten naar een logische formule (of omgekeerd), tot technisch vrij gesofisticeerde instrumenten waarmee men de student vraagt de correctheid van bepaalde logische uitdrukkingen aan te tonen of te weerleggen.
De webtoepassing bevat een aantal vragen die expliciet in de onderliggende databank werden ingebracht, maar ook heel wat opgaven die door de computer zelf automatisch worden gegenereerd en steeds moeilijker worden naarmate de student meer en meer opgaven van eenzelfde type correct oplost. Voor alle duidelijkheid willen we benadrukken dat het programma is ontworpen voor gebruik als zelfstudie-instrument en bijvoorbeeld niet dient voor het online afnemen van toetsen en examens.

Uitbreidingen

Er bestaan verschillende manieren om de formele logica aan te brengen bij studenten, afhankelijk van de context waarin deze logica later opnieuw aan bod zal komen, van de gangbare conventies in het vakgebied en van de persoonlijke voorkeuren van de lesgevers. Ook voor de vakken die het onderwerp vormen van deze aanvraag is er onderling een significant verschil in aanpak, die dan op zijn beurt grondig verschilt van wat er in de faculteit Letteren en Wijsbegeerte gangbaar is. De voornaamste verschillen betreffen syntax en bewijsvoeringsmethodiek (zie verder).
Er kan een klein gedeelte van het bestaande logicaprogramma min of meer ongewijzigd ingezet worden in de logicavakken van de faculteit Wetenschappen, maar dit onderdeel is zeer beperkt en zelfs dan nog moeten inhoud en vorm enigszins worden aangepast. We geven hiervan twee eenvoudige voorbeelden:

• Niet elke lesgever gebruikt dezelfde notatie voor hetzelfde begrip. Zo zijn er bijvoorbeeld reeds drie gebruikelijke notaties voor ‘als A dan B’ in omloop: A ⇒  B, A → B en A ⊃ B.
• Niet elke logicus is in elke context even strikt: soms mag je bijvoorbeeld in ((A & B) & C) de haakjes weglaten, soms mogen enkel de buitenste haakjes weg en soms is de geciteerde formule de enige die als welgevormd mag worden beschouwd.

Voor de leek lijken dit misschien details, maar als er een domein is waarin dergelijke details belangrijk zijn, dan is het wel de formele logica. De keuzes hebben niet alleen te maken met de persoonlijke smaak van de lesgever, maar zijn fundamenteel voor de manier waarop de theorie van de logica bij de studenten wordt geïntroduceerd. Ze zijn met andere woorden cruciaal om een student al dan niet een dergelijk zelfstudieprogramma te laten gebruiken.

Bewijsvoeringsmethodiek

Bovenstaande voorbeelden zijn syntactisch van aard. Het meest ingrijpende verschil tussen de vakken zit hem echter in de gebruikte methodiek voor bewijsvoering. Dit betekent dat twee van de meer geavanceerde onderdelen van het logicaprogramma (de tableau-methode en de bewijsinterface) niet kunnen gebruikt worden in de voornoemde vakken.

De belangrijkste (en technisch de meest ingewikkelde) uitbreiding waarvoor we dit project willen opzetten, is een module die toelaat om bewijsbomen en afleidingsbomen grafisch voor te stellen, door de studenten te laten bewerken en door de computer op correctheid te laten onderzoeken. Bewijsbomen en afleidingsbomen zijn conceptueel verschillend maar gelijkaardig van vorm. Op de volgende bladzijde hebben we een voorbeeld afgebeeld van elk van de twee types boom – binnen een online zelfstudietoepassing zullen ze er wellicht nog heel wat anders uitzien.

Het vak Redeneren, Abstraheren en Formuleren gebruikt geen grafische bewijsvoeringsmethode, maar volgt een calculationele benadering: enigszins zoals bij wiskundige formules bewijst men dat een logische formule waar is door ze af te leiden uit gekende ‘stellingen’ door onderdelen van formules te vervangen door equivalente onderdelen. Een module die nagaat of dergelijke equivalenties correct worden toegepast is technisch iets eenvoudiger te verwezenlijken dan de grafische methodes hierboven, maar toch niet meteen een sinecure.

Doelstellingen van het project + tijdsbesteding

Het project heeft tot doel een aantal bijkomende opgavetypes te programmeren en een aantal aanpassingen te implementeren zodat de huidige zelfstudietoepassing voor logica-oefeningen van de faculteit Letteren en Wijsbegeerte ook nuttig kan worden ingezet in de logica-gerelateerde vakken van de Informatica- en Wiskundeopleidingen. In detail gaat het om het volgende

1. (10%) Kleine aanpassingen betreffende notatie en welgevormdheid van formules.
2. (20%) Een grafische module die de gebruiker toelaat om bomen te editeren en manipuleren binnen een beperkte context.
3. (25%) Een nieuw opgaventype voor het maken en controleren van bewijsbomen, die gebruik maakt van deze grafische module.
4. (25%) Een nieuw opgaventype voor het maken en controleren van afleidingsbomen, die gebruik maakt van deze grafische module.
5. (20%) Een opgaventype voor het maken en controleren van bewijzen met de bewijscalculus uit Redeneren, Abstraheren en Formuleren.

Tussen haakjes staat steeds de geschatte relatieve tijdsbesteding nodig om het doel te bereiken.