GveCalc
Een Java programma voor formele logica
Het hier voorgestelde programma is een experimenteel tool voor
(o.a.) formele logica. De best uitgebouwde module op dit ogenblik
laat de gebruiker toe formele bewijzen uit de propositielogica
in te voeren en te verifiëren. De gebruikte set bewijsregels
is naar believen aan te passen. Ook een generator van
waarheidstabellen is geïmplementeerd. Op termijn is het
de bedoeling andere aanwezige modules verder uit te bouwen
(predikatencalculus, tableaumethodes, grafentheorie,
functieplotter) en andere toe te voegen en het geheel
flexibeler en daardoor makkelijker uitbreidbaar te maken:
gebruikergedefinieerde datatypes en operatoren,
Hoare-calculus (liefst over Java programma's),
namespace/package ondersteuning, ...
Er is redelijk wat aandacht besteed aan de interactie met de gebruiker;
zo worden de ingetikte formules bijvoorbeeld geparsed
tijdens het intikken zelf.
Het programma heeft al enkele maanden proef kunnen draaien bij de
lessen
Formele Logica
van prof. Hoogewijs
(2e kandidatuur Informatica, RUG). De ervaring valt, op
de klassieke kinderziekten na, positief uit, in zoverre dat de studenten
spontaan ontbrekende bewijsregels zelf begonnen aan te maken
(wat bij de vroeger gebruikte tools eerder ongebruikelijk bleek).
Een deel van de functionaliteit (in de praktijk vooral beperkt door
de hoeveelheid paranoia van de gebruikte webbrowser)
is beschikbaar rechtstreeks van het web
doordat het programma ook als applet ontwikkeld is.
Referenties
http://cage.rug.ac.be/~gvernaev/GveCalc/
Programma en handleiding