Recursive specifications and formal logic. What benefits for intelligent tutoring systems?

Abstract

The pedagogical assessment of a tutoring system relies upon a proof of convergence: for such a tutor the correction of student mistakes must not forever delay the teaching process. Such a tutor must provide uniform diagnosis in order to drive the dialog with the student. Student learning can be simulated by a·compilation of knowledge, but it is also necessary to compile knowledge for the teaching process. How can the tutor adjust these levels of compilation while keeping uniform diagnosis? We propose here to use recursive specifications, which consists of formalizing the definition of a class of problems at the same time as their solutions. Such a class "doesn't hide information": this allows its subsequent compilation.