Results 1 to 2 of 2

Math Help - Predicate Logic to prove equality of math formula

  1. #1
    Newbie
    Joined
    Jul 2012
    From
    Australia
    Posts
    1

    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
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,527
    Thanks
    773

    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 x_1^{a_1}\dots x_n^{a_n} where the sequence 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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 4
    Last Post: December 17th 2011, 11:48 AM
  2. set theory / predicate logic math language problem
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: December 7th 2010, 12:21 AM
  3. Replies: 2
    Last Post: March 26th 2010, 07:42 AM
  4. Predicate Logic
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: February 6th 2010, 06:23 AM
  5. predicate logic
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: March 6th 2009, 06:04 AM

Search Tags


/mathhelpforum @mathhelpforum