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 | next forum topic | other blogs | 767 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