OpenMath Content Dictionary: plangeo3

Canonical URL:
http://www.openmath.org/cd/plangeo3.ocd
CD Base:
http://www.openmath.org/cd
CD File:
plangeo3.ocd
CD as XML Encoded OpenMath:
plangeo3.omcd
Defines:
altitude, angle, arc, are_on_circle, center, center_of, center_of_gravity, circle, distance, is_midpoint, midpoint, parallel, perpbisector, perpendicular, perpline, polarline, radius, radius_of, tangent
Date:
2004-06-01
Version:
0 (Revision 3)
Review Date:
2006-06-01
Status:
experimental

This CD defines symbols for planar Euclidean geometry related to distance.

distance

Description:

The distance between two affine points is the Euclidean distance. The distance between two geometric objects O and O' is the infimum of the distances between two affine points, one on O and one on O'.

Example:
The distance between two points A and B.
$\mathrm{distance}\left(A,B\right)$
Signatures:
sts

 [Next: perpendicular] [Last: arc] [Top]

perpendicular

Description:

perpendicular is a binary boolean function with input two lines, halflines or segments. Its value is true whenever the two inputs are perpendicular to each other.

Example:
Testing perpendicularity of two lines L and M.
$\mathrm{perpendicular}\left(L,M\right)$
Signatures:
sts

 [Next: parallel] [Previous: distance] [Top]

parallel

Description:

parallel is a binary boolean function with input two lines, halflines or segments. Its value is true whenever the two inputs are parallel.

Example:
Testing parallelism of two lines L and M.
$\mathrm{parallel}\left(L,M\right)$
Signatures:
sts

 [Next: circle] [Previous: perpendicular] [Top]

circle

Description:

The symbol represents a circle. The circle may be subject to constraints.

Example:
The circle C with center A and radius 1 is given by
$\mathrm{circle}\left(C,\mathrm{center}\left(C,A\right),\mathrm{radius}\left(C,1\right)\right)$
Signatures:
sts

Description:

Example:
The assertion that the radius of the circle C is 1:
$\mathrm{radius}\left(C,1\right)$
Signatures:
sts

Description:

Gives the radius of a circle.

Example:
The radius of the circle C is given by
$\mathrm{radius_of}\left(C\right)$
Signatures:
sts

center

Description:

Defines the center of a circle.

Example:
The circle C with center A and radius 1 is given by
$\mathrm{circle}\left(C,\mathrm{center}\left(C,A\right),\mathrm{radius}\left(C,1\right)\right)$
Signatures:
sts

center_of

Description:

Gives the center of the circle

Example:
If C is the circle of the previous example then the following gives A.
$\mathrm{center_of}\left(C\right)$
Signatures:
sts

 [Next: are_on_circle] [Previous: center] [Top]

are_on_circle

Description:

The statement that a set of points is on one circle.

Example:
This example states that A, B, C, and D lie on one circle.
$\mathrm{are_on_circle}\left(A,B,C,D\right)$
Signatures:
sts

 [Next: angle] [Previous: center_of] [Top]

angle

Description:

Angle of a corner, always measured in positive (anti-clockwise) direction.

Example:
Notice that
$\mathrm{angle}\left(\mathrm{corner}\left(A,B,C\right)\right)$
$\mathrm{angle}\left(\mathrm{corner}\left(C,B,A\right)\right)$
are not the same.
Signatures:
sts

 [Next: midpoint] [Previous: are_on_circle] [Top]

midpoint

Description:

The midpoint between two points or two endpoints of a segment.

Example:
The midpoint of two points A and B is the same as the midpoint of the segment S on A and B.
$\mathrm{midpoint}\left(A,B\right)$
equals
$\mathrm{midpoint}\left(\mathrm{segment}\left(A,B\right)\right)$
Signatures:
sts

 [Next: is_midpoint] [Previous: angle] [Top]

is_midpoint

Description:

The statement that one point is the midpoint of two others.

Example:
This example states that C is the midpoint of A and B.
$\mathrm{is_midpoint}\left(C,A,B\right)$
Signatures:
sts

 [Next: center_of_gravity] [Previous: midpoint] [Top]

center_of_gravity

Description:

Center of gravity of a number of points.

Example:
The center of gravity G of three points A, B and C is defined as follows.
$\mathrm{point}\left(G,\mathrm{center_of_gravity}\left(A,B,C\right)\right)$
Formal Mathematical property (FMP):
$\mathrm{center_of_gravity}\left(A,B\right)=\mathrm{midpoint}\left(A,B\right)$
Signatures:
sts

 [Next: perpbisector] [Previous: is_midpoint] [Top]

perpbisector

Description:

Given two distinct points A and B, this is the line of all points at equal distance to both A and B.

Example:
$\mathrm{perpbisector}\left(A,B\right)$
Signatures:
sts

 [Next: altitude] [Previous: center_of_gravity] [Top]

altitude

Description:

Given a point p and a line L, this defines the segment starting at p and ending in the unique point of L closest to p.

Example:
$\mathrm{altitude}\left(p,L\right)$
Signatures:
sts

 [Next: perpline] [Previous: perpbisector] [Top]

perpline

Description:

Given a point p and a line L, this defines the line through p perpendicular to L.

Example:
$\mathrm{perpline}\left(p,L\right)$
Signatures:
sts

 [Next: polarline] [Previous: altitude] [Top]

polarline

Description:

Given a point p and a circle C this defines the polar line of p with respect to C.

Commented Mathematical property (CMP):
If p is incident with the circle C, the polar line of p with respect to C is the tangent line at p with respect to C.
Example:
$\mathrm{polarline}\left(p,C\right)$
Signatures:
sts

 [Next: tangent] [Previous: perpline] [Top]

tangent

Description:

Given a line L and a circle C this boolean checks whether L is a tangent line to C.

Example:
$\mathrm{tangent}\left(L,C\right)$
Signatures:
sts

 [Next: arc] [Previous: polarline] [Top]

arc

Description:

an arc of a circle M from A to B is the set of points of M that are encountered when traversing the circle clockwise from A to B.

Example:
$\mathrm{arc}\left(\mathrm{circle}\left(M\right),\mathrm{point}\left(A\right),\mathrm{point}\left(B\right)\right)$
Signatures:
sts

 [First: distance] [Previous: tangent] [Top]