MacKE: Yet Another Proof Assistant Automated Pedagogic Tool

. In this paper, we describe the implementation of (yet another) proof assistant and/or automated pedagogic tool. This one is based on the calculus KE and our Prolog implementation of free variable KE. The new system is written in LPA MacProlog TM , and features an interactive interface via menus, dialogues and graphics tools, a graphics window for constructing and displaying proofs, and on- and off-line proof checking. The ease of use and the visual satisfaction of the interface should make the system very convenient for fulfilling its primary intended function: teaching logic and reasoning through KE. 1 Introduction In this paper, we describe the implementation of (yet another) proof assistant and/or automated pedagogic tool. This one is based on the calculus KE [4] and our Prolog implementation of free variable KE [11]. KE is reviewed in Sect. 2.1, and our implementation is described in Sect. 2.2. The new system is written in LPA MacProlog TM , and features an interactive inter..