Automated Checking of
Flexible Mathematical Reasoning
in the Case of Systems of (In)Equations and
the Absolute Value Operator

Antti Valmari
University of Jyväskylä, Finland

We illustrate how our tool gives feedback when
the student solves challenging problems.

Let us solve this system of equations in Pólya's famous book:

 x + 7y + 3v + 5u =   16 ∧
8x + 4y + 6v + 2u = −16 ∧
2x + 6y + 4v + 8u =   16 ∧
5x + 3y + 7v +  u = −16

We try first a straightfoward approach:

• Solve x from the first equation.
• Assign it to the rest.

real_logic solve_all ok_text You solved it! Great! #<span style=#"font-size:xx-large#"#> 🍾#</span#> <=> x = 16-(7y + 3v + 5u) /\ 8(16-(7y + 3v + 5u)) + 4y + 6v + 2u = -16 /\ 2(16-7y + 3v + 5u) + 6y + 4v + 8u = 16 /\ 5(16-(7y + 3v + 5u)) + 3y + 7v + u = -16 or

Next solve y.

• “original ==>” saves us from copying the full system.

original ==> 128-56y-24v-40u + 4y + 6v + 2u = -16
<=> y = 144/52 -18/52 v -38/52 u

Pink feedback warns that the current final answer
solves a sub-task instead of the original task.

• Don't worry about that! We will carry on!

But the numbers look horrible! Is there an easier way?

real_logic solve_all ok_text You solved it! Great! #<span style=#"font-size:xx-large#"#> 🍾#</span#> x + 7y + 3v + 5u = 16 /\ 8x + 4y + 6v + 2u = -16 /\ 2x + 6y + 4v + 8u = 16 /\ 5x + 3y + 7v + u = -16 or

The second and third equation add nicely:

==> 8x + 4y + 6v + 2u = -16 /\ 2x + 6y + 4v + 8u = 16
==> 10x + 10y + 10v + 10u = 0

So do also the first and last:

original ==> 6x + 10y + 10v + 6u = 0

Subtracting them yields:

original ==> 4x + 4u = 0 <=> u = -x

We've made progress! And will make more:

original ==> 6x + 10y + 10v + 6u = 0 /\ u = -x
==> 10y + 10v = 0 <=> v = -y
original /*Exploit first equation*/==> x + 7y - 3y - 5x = 16 <=> -4x + 4y = 16
<=> y = x+4
original /*Exploit last equation*/==> 5x + 3y - 7y - x = -16 <=> 4x - 4y = -16
<=> y = x+4

Why did we get the same? Use subproof assume to see.

subproof assume u = -x /\ v = -y;
original <=> x + 7y + 3v + 5u = 16 /\ 5x + 3y + 7v + u = -16
<=> x + 7y - 3y - 5x = 16 /\ 8x + 4y - 6y - 2x = -16
<=> -4x + 4y = 16 /\ 6x - 2y = -16 <=> x = -2 /\ y = 2 subend

These yield the final answer:

original <=> x = -2 /\ y = 2 /\ v = -2 /\ u = --2

Conclusion

Students may solve significant problems at home.

• Our tool provides much of the necessary help and feedback.

The problems can be challenging enough to develop their logic and problem solving skills.

---

We have −40 °C = −40 °F and 100 °C = 212 °F. The Celsius
to Fahrenheit formula is F = aC + b. Solve a and b.
real_logic ok_text Oi­kein! f_nodes 9 solve_all hide_expr -40a + b = -40 /\ 100a + b = 212 <=>
or