Services & ResourcesWolfram ForumsMathGroup Archive

[Date Index] [Thread Index] [Author Index]

Re: Experimental`ImpliesQ, Help me understand it.

• To: mathgroup at smc.vnet.net
• Subject: [mg59228] Re: [mg59202] Experimental`ImpliesQ, Help me understand it.
• From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
• Date: Wed, 3 Aug 2005 01:19:37 -0400 (EDT)
• References: <200508020442.AAA16693@smc.vnet.net>
• Sender: owner-wri-mathgroup at wolfram.com

On 2 Aug 2005, at 06:42, Nasser Abbasi wrote:

>
> Hello;
>
> This 5.2 on windows.
>
> Starting from the logic that If sin^2+cos^2==q, then this implies q
> must be 1, so I typed:
>
> ------------
> Remove["Global`*"]
> Experimental`ImpliesQ[Sin[x]^2 + Cos[x]^2 == q, q == 1]
> Experimental`ImpliesQ[FullSimplify[Sin[x]^2 + Cos[x]^2 == q], q == 1]
>
> False
>
> True
>
> -------------
> From the help it says:
>
> "ImpliesQ returns False if it cannot determine whether a implies a,
> using any of its built-in transformation rules. "
>
> So, my question is, why did I have to fully simplify sin^2+cos^2==q to
> get True? I would think I should get True without it. As the help
> seems to say it will try all the build-in transformation rules?
>
> thanks,
> Nasser
>
>
>


ImpliesQ uses only "algebraic" transformation rules, as for example


Experimental`ImpliesQ[x^2+y^2==1,x^2==1-y^2]

True

The reason for that is that it relies on purely algebraic  
(essentially polynomial) algorithms (principally Cylindrical  
Algebraic Decomposition).
The relation Sin[x]^2+Sin[y]^2==1 is not algebraic and is not "known"  
to ImpliesQ.

Whey you used FullSimplify your formula was first converted to :

Experimental`ImpliesQ[1==q, q == 1]

which obviously is "algebraic" and hence ImpliesQ could determine  
that it is True.

Andrzej Kozlowski

• References:
  • Experimental`ImpliesQ, Help me understand it.
    • From: "Nasser Abbasi" <nma@12000.org>