Home » forums » LtU Forum

Proof system for learning basic algebra

I've written a system for learning basic algebra which has you solve problems by clicking on the rules of basic algebra (commutativity, associativity, etc.). It is impossible to make mistakes because the machine checks things like correct handling of division by zero. Each step is justified, so each solution serves as a formal proof. Right now it handles algebra up to quadratic equations and simultaneous equations.

It is intended to be a computer proof system anyone can learn. The style of mathematics presented mimics equation solving on a blackboard, so it should be familiar to everyone.

https://algebra.sympathyforthemachine.com/

By Edwin Zacharias at 2018-05-14 12:49 | LtU Forum | previous forum topic | next forum topic | other blogs | 2369 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

focus

I like the solution used to the subproblem of selecting focus on particular parts of the expression.

By John Shutt at Tue, 2018-05-15 13:51 | login or register to post comments

Nice feature of the interface

One very nice feature of the interface is that it handles complex examples just as easily as simple ones. Most equation manipulators I've seen become unusable for more complex equations.

Usability comments:
It takes three clicks to apply a transformation (Notes>Transformations>click). Changing the Notes menu into a row of buttons would reduce this to two clicks.

In the scratchpad the number entry method resembles a calculator, but a calculator has the entry button in the lower right, so I sometimes get confused and click zero instead of "ok". You might want add an enter or ok button in the lower right where "=" normally would be

The "level completed rectangle" was not self evident. The standard notation is a right pointing arrow that is greyed out until the level is completed.

When I am focused on a left branch of an expression it takes two clicks to focus on the right branch. I often click the wrong bubble because one decision (focus on THAT expression there) takes several clicks. (the whole focus tree should be navigable instead of node by node)

I like the ability to build expressions with the scratchpad. It would also be fun to compose transformations into new transformations, such as composing left distribution and commutativity of multiplications to create right distribution. I see you did this with transfer by negation and inversion.

What you have seems pretty cool

By Anders Horn at Fri, 2018-05-18 18:14 | login or register to post comments

Re: Nice feature of the interface

Thanks for the user interface suggestions. They all sound good.

I left out deriving custom transformations because I wanted to keep things as simple as possible. It's not quite powerful enough to manage it, but it would be nice to head in that direction.

By Edwin Zacharias at Sun, 2018-05-20 23:45 | login or register to post comments

UX

Could you make it where you select a sub-expression by clicking on the top level operator or leaf in the expression itself? That would be a lot more intuitive than the dots, I think.

By Matt M at Mon, 2018-05-21 01:42 | login or register to post comments

Possibly more bikeshedding

After thinking about it some more I realized that what bothered me about the focus navigation wasn't the amount of clicks (a click with 0 seek time can be almost the same as no click at all) but the mismatch between the visualization as a linear string of symbols, and the navigation as tree traversal. The operations I expect on a visual object are: zoom in/out and pan left/right. The operations I am provided —zoom out, left zoom, and right zoom— are perfectly good substitutes for zoom in/out, but pan left/right is tangibly missing. Every time I want to pan I must translate it into an arbitrary sequence of zooms.

The conflict between these two schemas is difficult to resolve because making the expressions more visibly tree-like might reduce students' knowledge transfer to situations outside your system.
But making the navigation more string-like might discourage students from conceptualizing it as a tree. Matt M's suggestion is probably the best way to resolve this because it still strongly emphasizes the tree nature of the expression, while requiring very little translation from perception to action.
(keep the current dots too)
(and when fingers get too fat to click accurately it is probably better to err towards selecting the operators rather than the leaves)

I also really like how the pallet of possible leaves is small enough to not be overwhelming but still allows you to add new ones.

When I am substituting a value for a meta-variable such as when I add A to both sides, I would like the transformation menu to turn into the full scratchpad, rather than just the leaf picker, so I could also choose a number or define a combination just when I needed it. And once I clicked the last "ok" to substitute it for the meta-variable I would be back in the transformations menu. 
(Having to back out of a transformation in order to define the expression I intend to use is a slight but noticeable speed-bump in the way of fluent operation.)

Also representing constraints on transformations such as x≠0 in the equation itself is a brilliant way of turning into an object something that most students have known only as a procedure.

By Anders Horn at Fri, 2018-05-25 02:23 | login or register to post comments

interfacing with text

This is a very good approach - it also allows for arbitrary transformations, I assume, so it could help to learn all kinds of algebras.

The hardest to learn about this system is the way that you let the user select. This is quite distracting, because selecting a part of a formula, or defining a focus, is usually done simply by dragging the cursor on the text directly.

Is there a reason why this couldn't be just a direct text interface where you select a part of a formula and are shown the transformations for that part? Just like you would select a bit of code in lisp and evaluate it?

Then this could even grow into a tool where you could modify the text and get shown which rule you have just applied (or that you stepped outside the rule system) - eventually how a fluent low-level proof assistant could work.

By Julian Rohrhuber at Fri, 2018-05-25 19:28 | login or register to post comments

... and

... and the same is true for the sketch pad and extra panels for combining expressions. It is hard to even remember what you were about to construct, because you don't see the terms when in the sketch pad. You could just let the user type them with the keyboard (aided by transformations).

(edited)

After going through the challenges a little more, I got used to the interface. The idea that you can navigate only to the end branches of the term tree (and having to use transformations like commutative law for navigational purposes) still strikes me as a little arbitrary. Is there a specific reason you allow only very specific selections?

Being able to judge what to select seems to me an important skill that could be learned through such a device.

By Julian Rohrhuber at Fri, 2018-05-25 20:27 | login or register to post comments