Bug in Resolve and Primes?

General discussion about Mathematica features and functionality...
Forum Rules
By using the Wolfram Faculty Program Forum, you agree not to post any abusive, obscene, vulgar, slanderous, hateful, threatening, or sexually oriented material. Wolfram Faculty Program Forum administrators have the right to remove, edit, move or close any topic at any time should we see fit.

Personal Information: Posts in this forum may be viewed by non-members; however, the forum prohibits non-members from viewing your profile. Although your email address is hidden from both non-members and members, your account is initially configured to allow members to contact you via email through the forum. If you wish to hide your profile, or prohibit others from contacting you directly, you may change these settings by updating your profile through the User Control Panel.

Attachments: Attachments are not currently enabled on this forum. To share a file with others on this site, simply upload your file to the online storage service of your choice and include a link to the file within your post. If your school does not offer an online file storage and sharing service, the following sites provide free basic online file storage and sharing: Mozy, FilesAnywhere, Adrive, and KeepandShare.

Bug in Resolve and Primes?

Postby David_Housman » Mon Oct 17, 2011 2:40 pm

I would have expected that the following two commands would return True and False, respectively. Instead, they are left in an unevaluated form.

Code: Select all
Resolve[ForAll[x, Implies[x == 2, Element[x, Integers]]]]
Resolve[ForAll[x, Implies[x == 2/3, Element[x, Integers]]]]


Mathematica should be able to handle the above commands because it can handle the logically equivalent forms below that make use of FindInstance.

Code: Select all
FindInstance[! Implies[x == 2, Element[x, Integers]], {x}] == {}
FindInstance[! Implies[x == 2/3, Element[x, Integers]], {x}] == {}


:?: Is there a bug with Resolve or is there something I do not understand? :?:

Worse, the following two commands return False and True, respectively, although they should both return True:

Code: Select all
Resolve[ForAll[{a, b}, Element[a, Primes] && Element[b, Primes], Implies[a^2 == b^2, a == b]]]
FindInstance[Element[a, Primes] && Element[b, Primes] && ! Implies[a^2 == b^2, a == b], {a, b}] == {}


:?: Perhaps there is a problem with Primes or my understanding of Primes? :?:
User avatar
David_Housman
 
Posts: 2
Joined: Fri May 13, 2011 7:32 pm
Organization: Goshen College
Department: Mathematics

Re: Bug in Resolve and Primes?

Postby Kathy_Bautista » Thu Oct 20, 2011 3:35 pm

Hello David,

I spoke to one of our Technical Support engineers, who mentioned that Resolve only attempts to remove the quantifier from the statement and simplify the statement. This is however a very good suggestion on how we can improve this functionality for a future version of Mathematica and he has forwarded this suggestion directly to the developers.

He also responded with the following...

"The customer may also be interested to know that FindInstance and Resolve work in very different ways. The internals are complicated, but the fundamental algorithm underlying each is incredibly different and what each does is a very different thing. Therefore the abilities of one of them does not really imply what the abilities of the other function should be in any way."

Here are the links to the documentation pages on both of these functions:


Let me know if you have any other questions.

-Kathy
Katherine Bautista
Senior Academic Program Manager
Wolfram Research, Inc.
http://www.wolfram.com
User avatar
Kathy_Bautista
Site Admin
 
Posts: 182
Joined: Fri Jul 31, 2009 6:24 pm
Location: Mesa, Arizona
Organization: Wolfram Research, Inc.
Department: Academic Initiatives

Re: Bug in Resolve and Primes?

Postby David_Housman » Fri Oct 21, 2011 2:14 am

Thank you for your response. Although I had read the documentation before, I decided to read it again.

Since every integer is a rational and since Mathematica documentation states, "Resolve[expr] can in principles (sic) always eliminate quantifiers for any Boolean expression expr," the following command should output True. Instead it returns the unevaluated expression.

Code: Select all
Resolve[ForAll[x, Implies[Element[x, Integers], Element[x, Rationals]]]]


Since Mathematica documentation states, "ForAll[x,cond,expr] is equivalent to ForAll[x,Implies[cond,expr]]," the following command should be equivalent to the proceeding command. Instead it returns True.

Code: Select all
Resolve[ForAll[x, Element[x, Integers], Element[x, Rationals]]]


The following command also outputs True.

Code: Select all
Resolve[ForAll[x, Implies[Element[x, Integers], Element[x, Rationals]]], Integers]


Based on this, it appears that the first command is unable to resolve the Boolean expression over the complexes, and so the second command is recognizing by the condition that the resolution should be over the integers.

While I would be amazed if the Mathematica function Resolve could "always eliminate quantifiers for any Boolean expression" as stated in the documentation, it is unsettling to find that it does not eliminate such an easy quantifier as in the first command. Or am I missing something in my logic?

The reason I find the above unsettling is because I planned to introduce Mathematica to my Discrete Mathematics students as a great way of computing mathematically defined concepts. Specifically, I had planned to define the following function, based on the first command above, for determining whether a set X is a subset of a set Y.

Code: Select all
Subset[X_, Y_] := Resolve[ForAll[x, Implies[Element[x, X], Element[x, Y]]]]


The corresponding mathematical definition comes directly from the text we are using. Unfortunately, as shown earlier, this function will not always return a Boolean value. I will instead provide a definition based on the second command, but that will not be as direct as the one based on the first command.

What is more unsettling is that the following command (as noted in my original post) returns False. This is WRONG!

Code: Select all
Resolve[ForAll[{a, b}, Element[a, Primes] && Element[b, Primes], Implies[a^2 == b^2, a == b]]]


How can I trust Mathematica on more complicated calculations when it gets a simple one wrong?
User avatar
David_Housman
 
Posts: 2
Joined: Fri May 13, 2011 7:32 pm
Organization: Goshen College
Department: Mathematics

Re: Bug in Resolve and Primes?

Postby Kathy_Bautista » Mon Oct 24, 2011 7:56 pm

Hi David,

I just sent you an email about this issue.

-Kathy
Katherine Bautista
Senior Academic Program Manager
Wolfram Research, Inc.
http://www.wolfram.com
User avatar
Kathy_Bautista
Site Admin
 
Posts: 182
Joined: Fri Jul 31, 2009 6:24 pm
Location: Mesa, Arizona
Organization: Wolfram Research, Inc.
Department: Academic Initiatives


Return to General Mathematica Discussion

Who is online

Users browsing this forum: No registered users and 2 guests

cron