Abstract

Current Status of the CMU Proof Tutor 3 The Proof Generator (the expert system) 3 The display-based prototype interface 3 Communication between the Proof Generator & the interface 4 Proposed Activities: What NCR Support Will Accomplish 4 Upgrading the VALID on-line course & integrating the Proof Tutor 5 Converting the VALID courseware to Kyoto Common Lisp 5 Integrating the Proof Tutor with the on-line course 5 Further enhancements to the on-line course 6 Implementing the display-based interface with help facilities 6 Formative evaluation + design of student model/diagnostician 6 Installing our translation facilities in the Proof Tutor 7 Extending the proof generating capability to predicate logic 7 Constructing on-line interactive tutorials on proof construction 7 Constructing a working student model/diagnostician 7 Significance, Impact & Visibility of the Proposed Project 8 Appendix: Brochure on the CMU Proof Tutor (With interface illustrations) 9