Features of the WinKE Software
The main purpose of the software is to lead students through a logic proof
step by step (in classical first-order predicate logic), but it can also
be used as an automated theorem prover. The WinKE process of constructing
a proof tree directly corresponds to what tradionally has been done using
pen and paper. The system is easy to use and visually
satisfying. The interactive graphical user interface consists of four windows:
the main window providing menus and buttons for quick access to the most
basic functions, the graphic window to display and manipulate KE proof
trees, a viewer which displays a scaled-down view of the virtual drawing
board, allowing to focus on a particular portion of it, and a tool box
containing several graphic tools.
The most important features of WinKE include:
-
three teaching modes for different levels of supervision and guidance,
respectively: pedagogue, supervisor, and assistant;
-
on- and off-line proof checking;
-
automated deduction;
-
automatic generation of countermodels;
-
visualisation for certain classes of countermodels (e.g. graphs or `pigeon
hole scenarios');
-
hints;
-
full control over proof trees through bookkeeping facilities and undo,
delete, and retract functions;
-
prepared files with sample problems;
-
editing of arbitrary new problem files directly within WinKE;
-
printing and generation of LaTeX tree descriptions;
-
software configuration to en/disable certain functions (you might, for
example, not want beginners to have access to the automated deduction feature,
etc.);
-
comprehensive help system.
To get a better impression you may also want to look at the screen
shots available on this site.
A free copy of WinKE will be sent
to you on request (email
Ulle
Endriss).
A list of known bugs is available here.
last modified on Friday, 17-Oct-2014 16:29:49 CESTby Ulle Endriss