Synthetic Geometry
The Wolfram Language provides not only extensive support for analytic geometry, but also support for the symbolic representation of synthetic geometry scenes in a form suitable for automated coordinate-independent reasoning.
Synthetic geometry scenes are represented in the Wolfram Language with GeometricScene. Scenes contain parameters representing named points and quantities, as well as hypotheses consisting of symbolic 2D regions and assertions involving those parameters. Conclusions can also be added to represent geometric theorems or conjectures that those hypotheses entail. Particular instances of a scene can be represented by specifying coordinates and values for all of the parameters appearing in the scene. Multiple instances of the same scene can be represented with a single GeometricScene object.
GeometricScene[{p1,p2,…},{hyp1,hyp2,…}] | abstract 2D geometric scene defined by the hypotheses hypi in terms of the symbolic points pi |
GeometricScene[{{p1,p2,…},{k1,k2,…}},hyps] | scene whose hypotheses depend on the symbolic scalar values ki |
GeometricScene[{p1{x1,y1},p2{x2,y2},…},hyps] | specific instance of a geometric scene with explicit coordinates for each point |
GeometricScene[{{p1{x11,y11},…},{p1{x21,y21},…},…},hyps] | collection of specific instances of a scene |
GeometricScene[…,…,{con1,con2,…}] | scene together with some conclusions coni about it |
GeometricScene[{scene1,scene2,…}] | combines several scene instances into one scene object |
Geometric scenes can be visualized by finding a particular instance of the scene using RandomInstance.
RandomInstance[scene] | find a random instance of a scene |
RandomInstance[scene,n] | find n instances |
Many 2D regions can be used as hypotheses in a geometric scene. All regions appearing in the hypotheses of a geometric scene are assumed to be nondegenerate and are displayed in instances of that scene:
AngleBisector[{p,q,r}] | infinite line bisecting the angle ∠ p q r |
Circle[p,r] | circle of radius r centered at the point p |
CircleThrough[{p1,p2,…}] | circle passing through the points pi |
Circumsphere[{p1,p2,p3}] | sphere passing through the points pi |
Disk[p,r] | filled disk of radius r centered at the point p |
HalfLine[{p,q}] | half-infinite line, or ray, starting at the point p and passing through the point q |
InfiniteLine[{p,q}] | infinite line passing through the points p and q |
Insphere[{p1,p2,p3}] | sphere tangent to the sides of the triangle △ p1 p2 p3 |
Line[{p1,p2,…}] | line segment passing through the points pi, in that order |
Midpoint[{p,q}] | midpoint of the line segment p q |
PerpendicularBisector[{p,q}] | perpendicular bisector of the line segment p q |
Point[p] | point p |
Polygon[{p1,p2,…}] | polygon with vertices pi |
RegionBoundary[reg] | boundary of the region reg |
RegionCentroid[reg] | centroid of the region reg |
RegionNearest[reg,p] | point closest to the point p in the region reg |
Triangle[{p,q,r}] | triangle with vertices p, q and r |
TriangleCenter[{p,q,r},spec] | center of triangle △ p q r specified by spec |
TriangleConstruct[{p,q,r},spec] | constructed geometric region defined by the triangle △ p q r specified by spec |
2D regions supported in GeometricScene.
Hypotheses can also be geometric assertions or equations involving geometric quantities defined on elements of the scene.
ArcLength[reg] | arc length of the region reg |
Area[reg] | area of the region reg |
EuclideanDistance[p,q] | Euclidean distance between the points p and q |
Perimeter[reg] | perimeter of the region reg |
PlanarAngle[{p,q,r}] | the measure of the angle ∠ p q r |
PolygonAngle[poly,p] | vertex angle of the polygon poly at the vertex p |
RegionDistance[reg,p] | distance from the point p to the region reg |
RegionMeasure[reg] | measure of the region reg |
SignedRegionDistance[reg,p] | signed distance from the point p to the region reg |
TriangleMeasurement[{p,q,r},spec] | measurement of the triangle △ p q r specified by spec |
Geometric quantities supported by GeometricScene.
p∈reg | assertion that the point p is an element of the region reg |
x1… | assertion that the regions/quantities xi are equal |
GeometricAssertion[objs,prop] | assertion that the objects objs satisfy the property prop |
GeometricStep[hyps,label] | step consisting of multiple hypotheses |
RegionMember[reg,p] | assertion that the point p is a member of the region reg |
Assertions supported by GeometricScene.
GeometricScene also supports style:
Style[objs,opts] | specify a style |
GeometricStylingRules | style all structures matching a pattern |
Specifying styles within GeometricScene.
The Wolfram Language can use these scene descriptions to find conjectures that may hold for a geometric scene.
FindGeometricConjectures[scene] | find conjectures that might hold for scene |
FindGeometricConjectures[{scene1,scene2,…}] | find conjectures that might hold for the instances scenei |
FindGeometricConjectures[scenes,patt] | find conjectures of the form patt |
FindGeometricConjectures[scenes,patt,n] | find up to n conjectures |
The Wolfram Language can perform logical reasoning on geometric scenes using such functions as GeometricSolveValues.
GeometricSolveValues[scene,expr] | solve for the symbolic geometric quantity expr defined by scene |
GeometricSolveValues[scene,{expr1,expr2,…}] | solve for multiple quanitites expr1,expr2, … defined by scene |
Reasoning on geometric objects can be done using GeometricTest.
GeometricTest[obj,prop] | test whether the geometric object obj satisfies prop |
GeometricTest[{obj1,obj2,…},prop] | test whether the obji satisfy prop |
GeometricTest[objs,prop1,prop2,…] | test whether objs satisfy each of the propi |