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

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