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:
To get a better impression you may also want to look at the screen
shots available on this site.
three teaching modes for different levels of supervision and guidance,
respectively: pedagogue, supervisor, and assistant;
on- and off-line proof checking;
automatic generation of countermodels;
visualisation for certain classes of countermodels (e.g. graphs or `pigeon
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,
comprehensive help system.
A free copy of WinKE will be sent
to you on request (email
A list of known bugs is available here.
last modified on Friday, 17-Oct-2014 16:29:49 CESTby Ulle Endriss