5. Current limitations and future work

The current prototype is a proof of concept aiming at demonstrating that the semantics of word problems can be handled given a formalization of the specific domain, a decision procedure on the resulting model, and a natural language application that allows to express and semantically interpret the facts describing the specific world instance.

In this work we have considered problems of a specific kind but we maintain that, in the e-Learning scenario, which is our target area of application, word problems can be classified according to schemes which can be formalized along the lines shown here. In many problems, understanding of natural language formulation is translated to facts in the knowledge base where two seemingly independent facts are put in a relation and become a new assumption for solving the problem (if A is an animal tamer, then A is not afraid of animals. if F is the father of S, then F is older than S. Every orange is a fruit). Construction of the correct assumption can be done in an exhaustive way only under a finite world assumption (what is known is what it is explicitly stated).

Future work

Replacing the Prolog engine by a proof assistant. These systems delivers proofs of propositions in a theory. By using a theory supporting a kind of word problems and forcing the problem author to express the problem as a a valid theorem in this theory would have the benefit of uncover hidden assumptions on the problem statement.

Also, these systems being more expressive than Prolog clauses, and supporting complex tactics for automatic proving could benefit the maintenance of the system.

On the student side, the discovering of new facts is converting into asserting propositions that can be transparently proved by tactics or presented to the student to deal with them: This would lead to re-using the same problem in different educations levels according to what is assumed and what is proved by the student.