From escobj@rpi.edu Wed Mar 19 16:20:53 1997 Received: from cs.rpi.edu (root@barney.cs.rpi.edu [128.213.3.4]) by mail1.its.rpi.edu (8.8.5/8.8.5) with ESMTP id QAA42712; Wed, 19 Mar 1997 16:20:52 -0500 Received: from dishwasher.cs.rpi.edu (escobarj@dishwasher.cs.rpi.edu [128.213.8.31]) by cs.rpi.edu (8.8.5/8.8.5) with SMTP id QAA03881; Wed, 19 Mar 1997 16:20:49 -0500 (EST) Sender: escobarj@cs.rpi.edu Message-ID: <333058AF.14CE@rpi.edu> Date: Wed, 19 Mar 1997 16:20:47 -0500 From: John Escobar X-Mailer: Mozilla 3.01Gold (X11; I; SunOS 5.5.1 sun4u) MIME-Version: 1.0 To: selmer@rpi.edu Subject: HTML and LaTex copies of the proposal Content-Type: multipart/mixed; boundary="------------15237D96809" X-UIDL: 34dc5744bf66739826ab767f840a3bd6 Status: R This is a multi-part message in MIME format. --------------15237D96809 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit I have attached the Latex and Html versions of the proposal. I will get a hardcopy of the proposal to you soon to be signed!! You can also get the HTML version at: http://www.cs.rpi.edu/~escobarj/project/proposal.html thanks, John P.S. I like the super-teaching web-page! --------------15237D96809 Content-Type: application/x-tex; name="proposal.tex" Content-Transfer-Encoding: 7bit Content-Disposition: inline; filename="proposal.tex" \documentstyle[psfig]{book} \textwidth 15.5cm \textheight 18.5cm \begin{document} COMPUTER SCIENCE PROJECT PROPOSAL PROVIDING A RICH VIRTUAL VISUAL/SYMBOLIC ENVIRONMENT FOR TEACHING REASONING BY JOHN ESCOBAR February 5, 1997 \begin{tabbing} Approved by: \= \>\hrulefill\ \hspace{.5in} \hrulefill\ \>Professor Selmer Bringsjord \hspace{.5in} \=Date \>Project Supervisor \>\hrulefill \>hrulefill \>Professor David Musser \>Date \>Sponsoring Faculty Member \end{tabbing} The problem can be stated in the following 3 questions: \begin{enumerate} \item How does one harness the reasoning power of machines with theorem provers to help people learn deductive reasoning? \item How does one combine visual and symbolic logic to teach deductive reasoning in a dynamic way? \item What role does visual reasoning and mental images (or diagrammatic reasoning) have with regard to computers? \end{enumerate} Reaching the following goals will mean solving a significant part of the above 1 and 2, and will lay part of the foundation for solving 3. \begin{enumerate} \item Drawing on both the Schubert Steamroller Problem (which is supplied as an example with OTTER; see Appendix for formalization of the problem) and the Dreadsbury Mansion Mystery (see Appendix for shot of DMM formalized in HYPERPROOF), create a tutorial that will enable students coming later to run OTTER on these examples, and thereby come to understand the relevant syntax, commands, etc. In both cases a knowledge base will be created, and commands relative to the knowledge base will be shown, with their effects. The tutorial should include sample input and output, and should refer to the OTTER Reference Manual. It should also include the results of some ``experimentation" on these problems. \item Use OTTER to implement a logic-based agent able to intelligibly navigate in the Wumpus World described in Russell \& Norvig's {\em Artificial Intelligence:~A Modern Approach}. (The functions {\sc Tell} and {\sc Ask}, for example, will be computed by OTTER. And the underlying knowledge base for this agent will consist of formulas in OTTER.) Furthermore, graphically display the Wumpus World in Java allowing for some minor interaction, such as allowing the user to place the wumpus on the grid. \item Intelligent 2nd-4th grade interactive logic tutor: \begin{enumerate} \item Create the mystery logic game ``Secrets" (which is a takeoff from the ``Number Sense" worksheet) using OTTER. \item Graphically display Secrets in Java, allowing the system to cue questions to the user depending on their ability to solve past questions, giving suggestions on the way. \end{enumerate} \item Relate the above work to the recent literature in AI on diagrammatic reasoning. This component of the project is expected to be short, but will lay part of the foundation for rich virtual visual/symbolic environments for teaching reasoning --- environments that push the envelope of diagrammatic reasoning in AI. \end{enumerate} The programs will be created in UNIX on the SUN Sparc Stations on my computer science account. Since there will be interaction with the user in Java while accessing OTTER it will be necessary to make a web-server that has permissions to my account where OTTER will be running. This project will be registered for 3 credits for the Spring 1997 term and 3 credits for the Fall 1997 term. \newpage \centerline{{\LARGE {\bf The Schubert Steamroller Problem}}} \input{schub.steam.tex} \newpage \centerline{{\LARGE {\bf The Dreadsbury Mansion Mystery}}} \vspace{.25in} Someone who lives in Dreadsbury Mansion killed Aunt Agatha. Agatha, the butler, and Charles live in Dreadsbury Mansion, and are the only people who live therein. A killer always hates his victim, and is never richer than his victim. Charles hates no one that Aunt Agatha hates. Agatha hates everyone except the butler. The butler hates everyone not richer than Aunt Agatha. The butler hates everyone Agatha hates. No one hates everyone. Agatha is not the butler. Now, given the above clues, there is a bit of a disagreement between three Norwegian detectives: Inspector Bjorn is sure that Charles didn't do it. Is he right? Inspector Reidar is sure that it was a suicide. Is he right? Inspector Olaf is sure that the butler, despite conventional wisdom, is innocent. Is he right? \begin{figure} \centerline{\psfig{figure=dread.prob.ps,height=3.5in}} \caption{Venn Diagrammatic Information for a Secrets Scenario} \end{figure} \end{document} --------------15237D96809 Content-Type: text/html; charset=us-ascii; name="proposal.html" Content-Transfer-Encoding: 7bit Content-Disposition: inline; filename="proposal.html" Project Proposal The problem can be stated in the following 3 questions:
  1. How does one harness the reasoning power of machines with theorem provers to help people learn deductive reasoning?
  2. How does one combine visual and symbolic logic to teach deductive reasoning in a dynamic way?
  3. What role does visual reasoning and mental images (or diagrammatic reasoning) have with regard to computers?

Reaching the following goals will mean solving a significant part of the above 1 and 2, and will lay part of the foundation for solving 3.

  1. Drawing on both the Schubert Steamroller Problem (which is supplied as an example with OTTER) and the Dreadsbury Mansion Mystery, create a tutorial that will enable students coming later to run OTTER on these examples, and thereby come to understand the relevant syntax, commands, etc. In both cases a knowledge base will be created, and commands relative to the knowledge base will be shown, with their effects. The tutorial should include sample input and output, and should refer to the OTTER Reference Manual. It should also include the results of some ``experimentation" on these problems.
  2. Use OTTER to implement a logic-based agent able to intelligibly navigate in the Wumpus World described in Russell & Norvig's Artificial Intelligence: A Modern Approach. (The functions TELL and ASK, for example, will be computed by OTTER. And the underlying knowledge base for this agent will consist of formulas in OTTER.) Furthermore, graphically display the Wumpus World in Java allowing for some minor interaction, such as allowing the user to place the wumpus on the grid.
  3. Intelligent 2nd-4th grade interactive logic tutor:
    1. Create the mystery logic game ``Secrets" (which is a takeoff from the ``Number Sense" worksheet) using OTTER.
    2. Graphically display Secrets in Java, allowing the system to cue questions to the user depending on their ability to solve past questions, giving suggestions on the way.
  4. Relate the above work to the recent literature in AI on diagrammatic reasoning. This component of the project is expected to be short, but will lay part of the foundation for rich virtual visual/symbolic environments for teaching reasoning -- environments that push the envelope of diagrammatic reasoning in AI.

The programs will be created in UNIX on the SUN Sparc Stations on my computer science account. Since there will be interaction with the user in Java while accessing OTTER it will be necessary to make a web-server that has permissions to my account where OTTER will be running.

This project will be registered for 3 credits for the Spring 1997 term and 3 credits for the Fall 1997 term. --------------15237D96809--