Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math

Topic: Formal Proof Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Andrew Tomazos

Posts: 137
Registered: 8/1/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 27, 2009 9:29 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Jun 27, 12:52 pm, Jan Burse <janbu...@fastmail.fm> wrote:
> Jan Burse schrieb:
>

> > Now we can continue working with multi sets. Lets
> > assume we have the multi sets for

>
> >    c + a = p1^s1 * ... * pk^sk = q * n * n
> >    c - a = q1^t1 * ... * qj^sj = q * m * m

>
> > Then q is the intersection of the two multi sets,
> > and the rest follows easily:

>
> >    q = intersect(c + a, c - a)
> >    n = sqrt(c + a / q)
> >    m = sqrt(c - a / q)

>
> > Bye
>
> Oops, I was jumping to conclusions. Are n and m
> necessarily coprime?
>
> In your theorem yes. When I started proving, no,
> I didn't require that.
>
> So the n, m are not unqiuely determined in my
> proof. When n and m are not coprime, then
> there is a factor u, such that
>
>      n = u * v
>      m = u * w
>
> Lets see what happens:
>
>      b = n * q * m = v * (q * u * u) * w
>      c + a = q * n * n = (q * u * u) * v * v
>      c - a = q * m * m = (q * u * u) * w * w
>
> Since the intersection will pick the greatest multi set
> that is in both multi sets, it will pick q * u * u.
>
> So my algorithm will deliver coprime n and m. And I
> now believe the intersect function is simply the gcd.
>
> So maybe we just need some theorems about gcd (greatest
> common divisor) and we are done?
>
> Bye
>
> Here is a computed example:
>
>    a = 5
>    b = 12
>    c = 13
>
>    c + a = 18
>    c - a = 8
>
>    q = gcd(c + a, c - a) = 2
>    n = sqrt(c + a / q) = 3
>    m = sqrt(c - a / q) = 2
>
>    b = n * q * m = 2 * 3 * 2 = 12 (yes)
>    c = q * (n*n + m*m) / 2 = 2 * (9 + 4) / 2 = 13 (yes)
>    a = q * (n*n - m*m) / 2 = 2 * (9 - 4) / 2 = 5 (yes)


Yes in this example (c + a / q) = 9 and (c - a / q) = 4. Both perfect
squares. How do you know that they will be perfect squares in all
cases?
-Andrew.


Date Subject Author
6/21/09
Read Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/26/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Joshua Cranmer
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Marshall
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Spiros Bousbouras
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Tim Smith
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Charlie-Boo
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
William Elliot
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/23/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
David Bernier
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.