Message Boards Message Boards

1
|
4377 Views
|
4 Replies
|
5 Total Likes
View groups...
Share
Share this post:

Get geometric conjectures about length using FindGeometricConjectures?

I have been enjoying the new GeometricScene and FindGeometricConjectures commands in v12. I have a question about the types of conjectures about lengths/distances that FindGeometricConjectures is able to come up with. In the examples I've seen and worked these seem to be of the form "these two distances are equal" or "this distance is equal to the sum of these distances". Is it possible to get conjectures about products of distances?

The example I was working on was the classic geometric construction of the square root of a positive number:

originalsqrt = 
 RandomInstance[ 
  GeometricScene[ {{a, b, c, d, e}, {r, s}}, {Line[ {a, b, c}], 
    b == Midpoint[{a, c}], d \[Element] Line[ {a, b}], 
    EuclideanDistance[ a, d] == 1,
     circle = Circle[b, EuclideanDistance[b, a]], 
    e \[Element] circle,
    GeometricAssertion[ {Line[{e, d}], Line[ {a, c}]}, 
     "Perpendicular"], r == EuclideanDistance[d, e], 
    s == EuclideanDistance[c, d]}], RandomSeeding -> 7]

enter image description here

In this picture r = the length DE is the square root of s = the length CD, or r^2=s: enter image description here

FindGeometricConjectures (at least the way I have this set up) does not come up this relationship. If I chain the classic "how to multiply two lengths" construction on top of this to multiply r by itself, r^2 becomes the length of AG in this scene:

fullsqrt = 
 RandomInstance[ 
  GeometricScene[ {a, b, c, d, e, f, g, h}, {Line[ {a, b, c}], 
    b == Midpoint[{a, c}], d \[Element] Line[ {a, b}], 
    EuclideanDistance[ a, d] == 1,
     circle = Circle[b, EuclideanDistance[b, a]], 
    e \[Element] circle,
    GeometricAssertion[ {Line[{e, d}], Line[ {a, c}]}, 
     "Perpendicular"],  Line[ {a, d, f}],  
    EuclideanDistance[a, f] == EuclideanDistance[d, e],
    ray = HalfLine[ {a, e}],
    g \[Element] ray, h \[Element] ray, 
    EuclideanDistance[h, a] == EuclideanDistance[ d, e], 
    GeometricAssertion[ {Line[{g, f}], Line[ {d, h}]}, "Parallel"]}], 
  RandomSeeding -> 7]

enter image description here

Now FindGeometricConjectures picks up that the length of AG (r^2) is the length of CD (s):

enter image description here

Is there a way to get this relationship to show up with FindGeometricConjectures in the original (and simpler) scene?
POSTED BY: Christopher Moretti
4 Replies
Sort By:

After thinking about this some more, I was able to get a partial solution from looking at several examples and noticing that when FindGeometricConjectures draws conclusions about similar triangles, it seems to order the vertices of the triangles in the corresponding order.

If that does always happen (and I realize that's an assumption on my part!), then you could form the equal ratios of lengths to get more information. I wrote this up as a function SimilarityBasedLengthConjectures, which takes in a geometric scene, adds all possible lines to the scene to encourage similarity checks, and tries to get the information from the equal ratios and any known distances included in the scene. I also added an option "SimilarityOnly", which when set to False adds any equations involving EuclideanDistance from the original conjectures to the mix. The code is in the attached notebook, and seems to get some new conjectures in some cases, including the "square root" one I started with above: new conjectures

Another example would be a regular pentagon with side length 1 and the "star" drawn inside:

pentagon = 
 RandomInstance[GeometricScene[ {a, b, c, d, e, f, g, h, i, j},
   {GeometricAssertion[ Polygon[ {a, b, c, d, e}], "Regular", 
     "Clockwise"],
    GeometricAssertion[{ Line[{a, c}], Line[ {b, e}]}, {"Concurrent", 
      f}],
    GeometricAssertion[{ Line[{a, d}], Line[ {b, e}]}, {"Concurrent", 
      g}],
    GeometricAssertion[{ Line[{a, c}], Line[ {b, d}]}, {"Concurrent", 
      h}],
    GeometricAssertion[{ Line[{c, e}], Line[ {b, d}]}, {"Concurrent", 
      i}],
    GeometricAssertion[{ Line[{a, d}], Line[ {c, e}]}, {"Concurrent", 
      j}],
    EuclideanDistance[a, b] == 1
    }], RandomSeeding -> 2]

pentagram

Using the "SimilarityOnly"->False option, lots of the individual lengths are found:

enter image description here

Attachments:
SimilarityBasedL...nb
POSTED BY: Christopher Moretti
Lin Cong
Lin Cong, Wolfram|Alpha
Posted 5 years ago

After thinking about this some more, I was able to get a partial solution from looking at several examples and noticing that when FindGeometricConjectures draws conclusions about similar triangles, it seems to order the vertices of the triangles in the corresponding order.

Yes, FindGeometricConjectures will only return one conclusion for each pair of similar triangles, with vertices corresponded.

I think the package proposed is very decent code, and it sure can extend the functionality of our built-in function. Thank you for your enthusiastic on the project. Are you familiar with our Wolfram function repository(https://resources.wolframcloud.com/FunctionRepository/), it is a public resource that allows third-party Wolfram Language extensions, and I think your project here can be one.

Also one trick about FindGeometricConjectures, there is an optional two-argument version, where you can specify the pattern of the conjectures, see https://reference.wolfram.com/language/ref/FindGeometricConjectures.html?q=FindGeometricConjectures

Hope this helps.
POSTED BY: Lin Cong
Updating Name
Updating Name
Posted 5 years ago

I didn't know about the Function Repository - after I finish tinkering with the code I will see about submitting it. There are a few improvements that shouldn't be too hard to make which should extend what it can find a bit more (in particular converting conjectured right angles to Pythagorean theorem statements about distances, converting Midpoint statements to equal distances, and directed Line/HalfLine objects to equations involving "total distance is sum of the parts"). I've been aiming at getting it to deduce results for scenes based on marked ruler constructions as my goal (I'm teaching a course this summer that includes a section on constructibility).
POSTED BY: Updating Name
Lin Cong
Lin Cong, Wolfram|Alpha
Posted 5 years ago

Thanks for exploring the new functionality! There currently is no way to get the relationship you are looking for in the original scene; however, as FindGeometricConjectures is an experimental function, we will add more functionalities in the future version, and the product relation of length looks like a good idea.
POSTED BY: Lin Cong
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Tag limit exceeded
Note: Only the first five people you tag will receive an email notification; the other tagged names will appear as links to their profiles.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract