Predicate Logic to prove equality of math formula

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

Re: Predicate Logic to prove equality of math formula

I am not sure how predicate logic would give you an algorithm for deciding if two expressions are equal. It seems that you need to decide if an equation follows from field axioms. The method that comes to mind is to normalize both sides and see if they are identical. Let's say you only deal with ring operations, i.e., polynomials. First, you need to order the variable names, for example, using alphabetical order. Then the standard form of a monomial would be $\displaystyle x_1^{a_1}\dots x_n^{a_n}$ where the sequence $\displaystyle x_1,\dots,x_n$ is ordered. Then you need to decide how to order monomials, probably again using some version of alphabetic order. After that, every expression should have a single normal form, which is a sum of monomials (possibly with coefficients) in the given order. Given two expressions, you can normalize them and compare their normal forms.

There may be smarter ways to define the normal form, for example, using Horner form. You may want to look at the paper "Proving Equalities in a Commutative Ring Done Right in Coq" by Benjamin Grégoire and Assia Mahboubi. It is pretty advanced, but you only need to get the idea and some implementation details.

Of course, dealing with fields is more complicated. Overall, I am wondering if it is easier to employ some computer algebra program and write a script that would ship an equation to it and return the result.