WinKE Home

WinKE: A Proof Assistant for Teaching Logic

WinKE is an interactive proof assistant based on the KE calculus, a refutation system which combines features from Smullyan's analytic tableaux and Gentzen's natural deduction. The software has been designed to serve as a tutoring system to support the teaching of logic and reasoning on an introductory level.

While originally designed as a Windows applications, WinKE will also run on other platforms, such as Linux (thanks to Wine).

To obtain a free copy of the latest version (currently 05/99) of the software please contact Ulle Endriss.

WinKE is supportive of an introductory textbook on classical logic (Marcello D'Agostino and Marco Mondadori, Logica, Edizioni Bruno Mondadori, 1997), but may also be used independently. WinKE has been used in courses on logic, automated reasoning, artificial intelligence, and philosophy at universities worldwide.

This web site provides access to a number of papers on WinKE and the underlying proof system KE, a short list of features supported by WinKE, some screen shots, a list of known bugs, and contact details.

WinKE Interface Image
Figure: A simple KE proof displayed by WinKE

last modified on Monday, 10-Nov-2008 08:27:08 CET by Ulle Endriss