人工智能在计算机辅助教学中的应用

本项目研究计算机辅助教学中的人工智能、专家系统和自动推理，以便研制既能自动推理又能交互式推理，能动态提示，自动审查学生证明步骤和自动批改作业软件系统。为达此目的我们必须有两种模型，一是自动推理模型，二是交互式推理模型，二者必须结合起来。为实现这两种模型，我们研究了算法。经过两年的实践，我们提出不使用SKOlem函数且能处理任何逻辑公式的合一算法。该算法已在计算机上实现，用该系统发现了Turing 机停机问题的机器证明和Andrews'挑战问题的机器证明。该结果发表在AAR Newsletter27 AAR协会主席Wos在该期前言中指出，本文是该期文章中最好的一篇。为解决搜索问题我们提出几个启发式搜索技术。