### Progress Report: 02/2005

###
Designing a Symbolic Solver for Arithmetic Constraints for Computer
Assisted Learning (*extended abstract*).

### 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

February 2005

## Abstract

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 [Tomás and Leal, PADL 2003],
for symbolic manipulation of sets and
exact arithmetic, that employ
CLP(Q) and
CLP(R) to some extent.