Predicate logic to prove equality of two formulas

[budihart]

Hi All,

I'm trying to write a program that will prove that a certain mathematical formula that is entered by a student is the same as the goal formula that I want.

For example, if the goal formula is: 2 * X + Y

then any of this student's answer can be considered correct:
-> X + X + Y
-> X - 5 + X + Y + 5
-> X/Y * Y + Y + X
-> Y + X * 2
and so on.

I have a thought that I can solve this problem by converting this mathematical formula to a predicate logic. But I still cannot figure out, how can I actually do it.

Any help is really appreciated.

Many thanks

 

[chiro]

Hi All,

I'm trying to write a program that will prove that a certain mathematical formula that is entered by a student is the same as the goal formula that I want.

For example, if the goal formula is: 2 * X + Y

then any of this student's answer can be considered correct:
-> X + X + Y
-> X - 5 + X + Y + 5
-> X/Y * Y + Y + X
-> Y + X * 2
and so on.

I have a thought that I can solve this problem by converting this mathematical formula to a predicate logic. But I still cannot figure out, how can I actually do it.

Any help is really appreciated.

Many thanks

Hey budihart and welcome to the forums.

The best way I recommend to doing this systematically is to user context-free grammars for representing these kinds of things.

What you do in order to show equivalence is to have procedures that simplify expressions as well as allow isomorphisms or 'equivalent transformations' between representations.

The simplification function part of your system will do things like implement all the algebraic functionality like expanding everything out into its full expanded parts while getting rid of redundancies (example X + X = 2X not X + X). You can do this with fairly simple algorithms for the algebra, and you can use a recursive procedure to collect common terms together.

The transformation part of the algorithm allows you to do more advanced things like recognize things that are equivalent but algebraicly hard or impossible to show. Something like say e^x and its taylor series expansion (1 + x + x^2/2 + ...) is one way, but you can make this as complex as you want by allowing integral and derivative expansions and all kinds of series expansions.

I know you probably won't do the second part, but if you want to extend it and make it powerful with a simple design, this is what I would recommend.

The language itself would best be represented with a binary tree. Each node would have some kind of operator and the tree itself would expand both left and right down to the leaves where each node has the information for that particular thing. It could be a number, a variable of different types, a linguistic expression, an integral or other evaluation, a series expansion, and so on.

If you use C++, you can create a class system that allows you to extend the node types and deal with specialized simplification and transformation.

The binary tree example is a good way to design for example, simple calculator programs that take expressions (including with parentheses) and expand them out to give a final answer.

If you need more clarification don't hesitate to ask.

 

[viraltux]

Hi All,

I'm trying to write a program that will prove that a certain mathematical formula that is entered by a student is the same as the goal formula that I want.

For example, if the goal formula is: 2 * X + Y

then any of this student's answer can be considered correct:
-> X + X + Y
-> X - 5 + X + Y + 5
-> X/Y * Y + Y + X
-> Y + X * 2
and so on.

I have a thought that I can solve this problem by converting this mathematical formula to a predicate logic. But I still cannot figure out, how can I actually do it.

Any help is really appreciated.

Many thanks

Hi budihart,

Adding to chiro's answer, you can write your program in just a few lines of code using Maxima as the core engine.

Now, if you are actually interested in how to do that yourself chiro has already given you a few hints; In CS this kind of analysis is called parsing. If you want to learn more about the theory behind parsing you can download a free book about parsing techniques from this site http://dickgrune.com/Books/PTAPG_1st_Edition/

Also, since Maxima is a FOSS project you can hack their code in whatever way you want and see how their parsers work too.

So Good Luck!

Edit: Maybe this question should be moved to the Computing & Technology forum, people checking that forum might have something else to say.