The Interactive Geometry Software Cinderella

Forum: Cinderella Support (E)

Forums->Cinderella Support (E)->Why doesn't the prover find the two points on this circle?

DavidBakin
3 stars
Why doesn't the prover find the two points on this circle?


In the attached construction I've built the configuration described at http://www.ics.uci.edu/~eppstein/junkyard/5circle.html - given the free lines L0..L4 the result should be that the 5 points P0..P4 are concyclic. Having constructed P0..P4 (they're the points that are yellow) I use the define-circle-through-3-points tool to put a circle through P0, P1, and P4 - that's the yellow circle. Clearly P2 and P3 are on the circle (you can move the lines L0..L4 arbitrarily and see this). But looking at the circle's definition in the Information Window it doesn't show that it is incident with P2 and P3. Why not? I thought the prover was supposed to discover things like this.

Thanks! — David

attachment 5 Circle Theorem.cdy (6.94 Kb)
attachment 5 Circle Theorem.cdy (6.94 Kb)
 
on: Sat 14 of Feb, 2009 [01:06 UTC] reads: 137574

Posted messages

author message
Aw: Why doesn't the prover find the two points on this circle?
on: Mon 16 of Feb, 2009 [20:04 UTC]
Hi,

sorry to join the conversation late, and thanks a lot to Wolf-Dieter!! Indeed, this is currently the only way to find the results of the prover, but I'll file a feature request that this piece of information should also be available in the inspector!

Ulli

author message
Heker
3 stars
Aw: Why doesn't the prover find the two points on this circle?
on: Mon 16 of Feb, 2009 [12:15 UTC]
> In the attached construction I've built the configuration described at http://www.ics.uci.edu/~eppstein/junkyard/5circle.html - given the free lines L0..L4 the result should be that the 5 points P0..P4 are concyclic. Having constructed P0..P4 (they're the points that are yellow) I use the define-circle-through-3-points tool to put a circle through P0, P1, and P4 - that's the yellow circle. Clearly P2 and P3 are on the circle (you can move the lines L0..L4 arbitrarily and see this). But looking at the circle's definition in the Information Window it doesn't show that it is incident with P2 and P3. Why not? I thought the prover was supposed to discover things like this.
>
> Thanks! — David

David,
I don't know why P2,3 are not on the list of incidences. But when you try to construct a circle through P2,P3,P4, you will see a message in the console window telling that the new circle is identical with the other. So the theorem proover seems to be ok.
Wolf-Dieter?

author message
DavidBakin
3 stars
Re: Aw: Why doesn't the prover find the two points on this circle?
on: Mon 16 of Feb, 2009 [19:19 UTC]
Hmm ... maybe I answered too soon ... I can't find how to get the console window to show up. I did discover that if I have the construction text window up then when I create the circle through P2,P3,P4 it highlights the circle P1,P0,P4, showing that it is the same circle.

-- David

author message
DavidBakin
3 stars
Re: Re: Aw: Why doesn't the prover find the two points on this circle?
on: Mon 16 of Feb, 2009 [19:31 UTC]
NEVER MIND! I found it at Views/Information Window ... which I hadn't tried because I assumed it was talking about ... you know, the Information Window (which is what you get from Edit/Information or ^I. (That's a bit confusing ...)

-- David

> Hmm ... maybe I answered too soon ... I can't find how to get the console window to show up. I did discover that if I have the construction text window up then when I create the circle through P2,P3,P4 it highlights the circle P1,P0,P4, showing that it is the same circle.
>
> — David

author message
DavidBakin
3 stars
Re: Aw: Why doesn't the prover find the two points on this circle?
on: Mon 16 of Feb, 2009 [19:08 UTC]
OK - I'll keep in mind the idea of "double checking" the incidences by creating a geometric object and looking in the console window. Thanks! — David



Show posts:
 
Cinderella
Language