Applying formal methods and representations in a natural language tutor to teach tactical reasoning

Past research has shown that students demonstrate learning gains even when the computer-based tutor can only partially understand a student's natural language answers. Our aim is to move towards even more effective natural language tutors that fully understand dialog. Coupled with high-fidelity simulations, such a tutor could provide substantial in-depth training, and engage the student in a detailed discussion of complex domains, such as military tactical reasoning. Our approach to effective natural language communication is to restrict the dialog to a manageable but expressive subset of natural language, to provide an English to logic translator, and to use ontologies to support knowledge-rich and highly context-dependent reasoning. By restricting grammatical patterns to a manageable subset we provide a robust and predictable natural language interface. Our translator, CELT (Controlled English to Logic Translation), translates sentences and queries in the CELT grammar into first-order logic. The lexicon is built on WordNet. Background knowledge is provided by the Suggested Upper Merged Ontology (SUMO). This generic lexicon and upper ontology can be extended with both domain-specific lexicons and domain-specific ontologies. The CELT translator uses Discourse Representation Theory (DRT) to represent multiple sentences and to provide a principled means of resolving anaphoric references. A first-order logic (FOL) theorem prover, such as SNARK [1], provides the highly context-dependent reasoning required to understand student questions to the tutor- and conversely to assess student answers to the tutor's questions. We have implemented the CELT translator, SUMO, CELT lexicon, and question-answering capabilities (CELT to logic, use of theorem prover, and back to English). We are in the process of implementing student query assessment. We also expect this tool suite to have other applications to intelligent tutoring systems and natural language tutors. For example, it should facilitate authoring for the description of domain-specific procedures, discourse-management procedures, and pedagogical procedures provided that suitable discourse and pedagogical ontologies are added.