A Computer Tutor for Formal & Applied Logic: A Proposal to NCR Corporation

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