Technical Report: DCC-2005-06

Designing a Symbolic Solver for Arithmetic Constraints for Computer Assisted Learning

Ana Paula Tom├ís, Nelma Moreira, Nuno Pereira

DCC-FC & LIACC, Universidade do Porto
R. do Campo Alegre 823, 4150-180 Porto, Portugal
Phone: 351 22 6078830, Fax: 351 22 6003654
E-mail: {apt,nam,nfp} @ dcc . fc . up . pt
May 2005


We present a solver for arithmetic and membership constraints over real numbers, for computer assisted learning (CAL) in math. The solver works as a rewrite system. What makes it novel are the proposed rewriting rules that go beyond simple algebraic reductions. Instead they work at high abstraction level and use some knowledge about the functions behaviour to shortcut solving steps. Designed with pedagogic concerns, they are useful to produce step-by-step solutions that look like ones worked out by students. In this way the solver may be more advantageous in some learning environments than sophisticated mathematical software, which is certainly the choice for scientific applications and advanced algebraic manipulations. The proposed solver is correct and although it is complete for a relevant set of problems arising in high-school math curricula, it is incomplete in general. Indeed, this is inherent to the addressed problem. A prototype is being developed in Prolog for a specific application domain, reusing some modules of Demomath for symbolic manipulation of sets and exact arithmetic, that employ CLP(Q) and CLP(R) to some extent. This work is part of AGILMAT project in which a web application to automatically generate and solve math drills is being developed.