Specialised theorem-proving in an intelligent tutoring system for the Dijkstra-Gries programming methodology

Ego is a goal-oriented intelligent tutoring system for disciplined programming (E.W. Dijkstra, 1976), strictly following the methodology in D. Gries´s (1981) monograph for simultaneously developing a program and its proof of correctness. It contains utilities to manipulate arithmetic and logical expressions, a weakest precondition calculator, models of students´ understanding, and theorem-proving facilities, as well as knowledge of the semantics of the programming language, steps of the methodology, and theorems relevant to proofs of correctness. We report on the theorem-proving facilities. They are specialised to the programming methodology and to the tutoring system