Automated Planar Geometry in Wolfram Language

Daniel McDonald, Wolfram Research
Peter Barendse, Wolfram Alpha

(RowDefault[, (Spacer1), , (Spacer1), ])  #WolframTechConf

Introducing GeometricSolveValues

Daniel McDonald, Wolfram Research

(RowDefault[, (Spacer1), , (Spacer1), ])  #WolframTechConf

ABSTRACT

Coming soon in Version 14.0, GeometricSolveValues[scene, expr] solves for the symbolic geometric quantity expr defined by the GeometricScene object scene.

Example 1

Represent Thales’ Theorem:

scene=GeometricScene[{a,b,c,d},{
Triangle[{a,b,c}],
CircleThrough[{a,b,c},d],
Line[{a,d,c}]
}];

Visualize it:

instance=RandomInstance[scene]

Solve for the angle at b in this particular scene instance:

GeometricSolveValues[instance,PolygonAngle[Triangle[{a,b,c}],b]]

Try to solve for the angle at b in general:

GeometricSolveValues[scene,PolygonAngle[Triangle[{a,b,c}],b]]

Example 2

Consider a triangle where one point has an unknown but positive x value:

scene=GeometricScene[{{a,b,c},{x}},{
a=={0,0},b=={0,4},
c=={x,5},x>0,
Polygon[{a,b,c}]
}];
instance=RandomInstance[scene]

Compute the area of the particular triangle pictured above:

GeometricSolveValues[instance,Area[Polygon[{a,b,c}]]]

Compute the area of the triangle for any value of x:

GeometricSolveValues[scene,Area[Polygon[{a,b,c}]]]

Example 3

Consider a scene featuring a right triangle with its leg lengths specified but its hypotenuse h unknown:

scene=GeometricScene[{{a,b,c},{h}},{
PolygonAngle[{a,b,c},a]==90Degree,EuclideanDistance[a,b]==1,
EuclideanDistance[a,c]==2,
h==EuclideanDistance[b,c]
}];
RandomInstance[scene]

The subvalue “AlgebraicFormulation” of a GeometricScene object gives a conjunction of constraints for that scene to be valid:

formulation=scene["AlgebraicFormulation"]

The hypotenuse h can be solved for using SolveValues on the algebraic formulation, or using GeometricSolveValues directly on the scene:

{SolveValues[Exists[{(IndexedDefault[a, 1]),(IndexedDefault[a, 2]),(IndexedDefault[b, 1]),(IndexedDefault[b, 2]),(IndexedDefault[c, 1]),(IndexedDefault[c, 2])},formulation],h,Reals],GeometricSolveValues[scene,h]}

More Examples

Solve for the area of a triangle

scene=GeometricScene[{a,b,c,d},{
EuclideanDistance[a,c]==10,
EuclideanDistance[b,d]==6,
EuclideanDistance[d,c]==5,
PlanarAngle[{b,a,d}]==2*PlanarAngle[{d,a,c}],
Line[{b,d,c}],
t==Style[Triangle[{a,b,c}],Orange]
}];
RandomInstance[scene]
GeometricSolveValues[scene,Area[t]]

Solve for the area of a quadrilateral

scene=GeometricScene[{a,b,c,d,e,f},{
PlanarAngle[{b,a,c}]==90Degree,
PlanarAngle[{a,c,b}]==45Degree,
Line[{a,d,c}],
Line[{b,f,c}],
Line[{a,e,b}],
Line[{e,f}],
GeometricAssertion[{Line[{d,f}],Line[{b,c}]},"Perpendicular"],
EuclideanDistance[a,d]==4,
EuclideanDistance[d,c]==8,
EuclideanDistance[a,e]==10,
p==Style[Polygon[{a,e,f,d}],Orange]
}];
RandomInstance[scene]
GeometricSolveValues[scene,Area[p]]

Solve for an angle

scene=GeometricScene[{a,b,c,p,q},{
PlanarAngle[{a,b,c}]==100Degree,
EuclideanDistance[a,b]==EuclideanDistance[b,c],
Line[{b,p,c}],
Line[{a,q,c}],
PlanarAngle[{b,a,p}]==30Degree,
PlanarAngle[{q,b,c}]==30Degree,
Style[PlanarAngle[{a,p,q}],Orange]
}];
RandomInstance[scene]
GeometricSolveValues[scene,PlanarAngle[{a,p,q}]]

Solve for the distance between two points

scene=GeometricScene[{a->{0,0},b,c,d,e,f},{
PlanarAngle[{c,b,e}]==PlanarAngle[{b,a,d}]==PlanarAngle[{a,d,c}]==90Degree,
Line[{a,e,d}],Style[Line[{a,f,c}],Orange],Line[{b,f,e}],
EuclideanDistance[a,e]==6,
EuclideanDistance[b,f]==6,
EuclideanDistance[e,d]==3,
EuclideanDistance[a,b]==EuclideanDistance[b,c]
}];
RandomInstance[scene]
GeometricSolveValues[scene,EuclideanDistance[a,c]]

Update on FindGeometricProof[...]

Peter Barendse, Wolfram Alpha

(RowDefault[, (Spacer1), , (Spacer1), ])  #WolframTechConf

ABSTRACT

Presented at previous WTC and still under development, FindGeometricProof produces a new ProofObject, containing a human-readable elementary proof of synthetic geometry facts and theorems, as well as graphical and computable representations and other properties of the proof.

Example 1

Find the base length, in meters, of a triangle from the area and altitude and produce a classic two-column proof:

scene = 
GeometricScene[{{"y","w","z","x"},{}},{
Line[{"y","w","z"}],
EuclideanDistance["x","w"]==(Quantity[3, "m", meters, "Meters"]),
Area[Triangle[{"y","z","x"}]]==(Quantity[13, (("m")^2), meters squared, (("Meters")^2)]),PlanarAngle[{"y","w","x"},"Counterclockwise"]==90 °
}];

pf=FindGeometricProof[EuclideanDistance["y","z"]==_,scene]

pf["Result"]

pf["ProofNotebook"]

(Clicking on a fact will print it in standard WL.)

Example 2

This example is simple enough that proving ‘All’ facts does not produces too many facts:

scene = 
GeometricScene[{{x,y,z,w,u,v},{}},
{
GeometricAssertion[{Line[{x,y}],Line[{z,w}],Line[{u,v}]},"MatchingParallel"],
Line[{x,z,u}],
PlanarAngle[{y,x,z},"Counterclockwise"]==30 °
}
];

RandomInstance[scene]

pf=FindGeometricProof[All,scene]

pf["ProofNotebook"]

pf["ProofGraph"]

Example 3

Solve an advanced high school example using Ptolemy’s Theorem:

RandomInstance[
PtolemysTheoremExample = 
GeometricScene[{{a,b,c,o},{}},
{
PlanarAngle[{b,a,c},"Counterclockwise"]==90°,
EuclideanDistance[b,a]==24,EuclideanDistance[c,a]==7,
CircleThrough[{a,b},o],
PlanarAngle[{c,o,b},"Counterclockwise"]==90°
},{}
]
]

proof = FindGeometricProof[EuclideanDistance[c,o]==_?NumericQ,PtolemysTheoremExample]

proof["Result"]

proof["ProofNotebook"]

Example 3

Find the value of the golden ratio using similar rectangles:

goldenScene = GeometricScene[{{"A","a","b","B","c","d"},{}},{
GeometricAssertion[{Polygon[{"A","a","b","B"}],Polygon[{"B","A","d","c"}]}, "Similar"], 
EuclideanDistance["A","B"]==EuclideanDistance["a","d"],GeometricAssertion[{Line[{"a","b"}],Line[{"A","B"}],Line[{"d","c"}]},"MatchingParallel"],GeometricAssertion[{Line[{"A","d","a"}],Line[{"B","c","b"}]},"MatchingParallel"],EuclideanDistance["A","a"]==3,PlanarAngle[{"A","a","b"},"Counterclockwise"]==Pi/2
}];

RandomInstance[goldenScene]

proof=FindGeometricProof[
_==1/GoldenRatio,
goldenScene
]

proof["ProofNotebook"]

proof["ProofGraphManipulate"]

Thank you for listening