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.independent

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 26, 2009 10:07 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Jun 26, 12:30 am, Jan Burse <janbu...@fastmail.fm> wrote:
> Andrew Tomazos schrieb:
>

> > On Jun 22, 4:01 am, Jan Burse <janbu...@fastmail.fm> wrote:
> >> b*b = (c+a) * (c-a)
> >> n*q*m*n*q*m = n*q*n * q*m*m    (factorization of b, c+a, c-a sic!)

>
> > In this step you have used:
>
> >   b = n*q*m
> >   c+a = q*n*n
> >   c-a = q*m*m

>
> > How do you know that there exists n, q and m such that these three
> > equalities hold?
> >   -Andrew.

>
> By some pingeonhole principle.
>
> n, q and m are classes of factors of b. If a class c is empty
> then c=1. If a class c contains factors j, k, etc.. then c=j*k*...
> So the n, q and m are not itself necessary prime, they group
> certain prime number factors.
>
> Each factor of b occurs twice in b*b, so b*b=n*q*m*n*q*m is trivial.
>
> And thus (c+a)*(c-a)=n*q*m*n*q*m follows also, since factors are unique,
> the same classes also occure in the product (c+a)*(c-a).
>
> 1) Now if a factor does not occur in (c+a) then it occurs twice in
> (c-a), this is the class m.
>
> 2) Further if a factor does not occur in (c-a) then it occurs twice in
> (c+a), this is the class n.
>
> 3) If a factor does not (not occur in (c+a) and not occur in (c-a)),
> then it occurs in (c+a) and it occurs in (c-a), this is the class q.


We can assume that theorems about the nature of integer factorization
have previously been established - but which ones specifically would
we use to prove your above statements?

I think it would be beneficial if we could compute q, n and m
directly.

Perhaps we can define a divisble_by function. So for example:

(12 divisable_by 4) == true
(12 divisable_by 5) == false

Then we could use facts about that function such as:

forall x, k in N
given:
x divisble_by k
implies:
thereexists y in N
x = y*k

forall x, y, k in N
given:
x divisible_by k
implies:
(x*y) divisible_by k

forall x, y, z, k in N
given:
z = x*y
z divisble_by k
implies:
(x divisble_by k) or (y divisble_by k)

What do you think? Which of these kind of theorems should we use as a
basis?
-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.