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

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