Home Overview Documents Content Dictionaries Software & Tools The OpenMath Society OpenMath Projects OpenMath Discussion Lists OpenMath Meetings Links

# OpenMath Content Dictionary: plangeo1

Canonical URL:
http://www.win.tue.nl/~amc/oz/om/cds/plangeo1.ocd
CD Base:
http://www.openmath.org/cd
CD File:
plangeo1.ocd
CD as XML Encoded OpenMath:
plangeo1.omcd
Defines:
assertion, configuration, incident, line, point, type, are_on_line
Date:
2004-06-01
Version:
0 (Revision 5)
Review Date:
2006-06-01
Status:
experimental

This CD defines symbols for planar Euclidean geometry.

## point

Description:

The symbol is used to indicate a point of planar Euclidean geometry by a variable. The point may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments.

Example:
Given two lines l and m, a point A on l and m is defined by:
$\mathrm{point}\left(A,\mathrm{incident}\left(A,l\right),\mathrm{incident}\left(A,m\right)\right)$
Signatures:
sts

 [Next: line] [Last: are_on_line] [Top]

## line

Description:

The symbol is used to indicate a line of planar Euclidean geometry by a variable. The line may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments.

Example:
Given points A and B, a line l through A and B is defined by:
$\mathrm{line}\left(l,\mathrm{incident}\left(A,l\right),\mathrm{incident}\left(B,l\right)\right)$
Signatures:
sts

 [Next: incident] [Previous: point] [Top]

## incident

Description:

The symbol represents the logical incidence function which is a binary function taking arguments representing geometric objects like points and lines and returning a boolean value. It is true if and only if the first argument is incident to the second.

Example:
That a point A is incident to a line l is given by:
$\mathrm{incident}\left(A,l\right)$
Signatures:
sts

 [Next: configuration] [Previous: line] [Top]

## configuration

Description:

The symbol represents a configuration in Euclidean planar geometry consisting of a sequence of geometric objects like points, lines, etc, but also of other configurations.

Example:
The configuration of a point A and a line l incident to A is defined by:
$\mathrm{configuration}\left(\mathrm{point}\left(A\right),\mathrm{line}\left(l,\mathrm{incident}\left(A,l\right)\right)\right)$
Example:
The prevous configuration of a point A and a line l incident with A can be extended by adding a second point B incident with l:
$\mathrm{configuration}\left(\mathrm{configuration}\left(\mathrm{point}\left(A\right),\mathrm{line}\left(l,\mathrm{incident}\left(A,l\right)\right)\right),\mathrm{point}\left(B,\mathrm{incident}\left(B,l\right)\right)\right)$
Example:
We describe a triangle on the distinct points A, B, C and lines a, b, c:
$\mathrm{configuration}\left(\mathrm{point}\left(A\right),\mathrm{point}\left(B,¬\left(A=B\right)\right),\mathrm{line}\left(c,\mathrm{incident}\left(c,A\right),\mathrm{incident}\left(c,B\right)\right),\mathrm{point}\left(C,¬\mathrm{incident}\left(C,c\right)\right),\mathrm{line}\left(a,\mathrm{incident}\left(a,B\right),\mathrm{incident}\left(a,C\right)\right),\mathrm{line}\left(b,\mathrm{incident}\left(b,A\right),\mathrm{incident}\left(b,C\right)\right)\right)$
Signatures:
sts

 [Next: type] [Previous: incident] [Top]

## type

Description:

The symbol represents the type of the basic geometric objects: points, lines, configuration.

Commented Mathematical property (CMP):
If A and B are objects of the same type, then they are not incident.
Formal Mathematical property (FMP):
$\mathrm{type}\left(A\right)=\mathrm{type}\left(B\right)⇒¬\mathrm{incident}\left(A,B\right)$
Signatures:
sts

 [Next: assertion] [Previous: configuration] [Top]

## assertion

Description:

The symbol is a constructor with two arguments. Its first argument should be a configuration, its second argument a statement about the configuration, called thesis. When applied to a configuration C and a thesis T, the OpenMath object assertion(C,T) expresses the assertion that T holds in C.

Example:
The assertion that two distinct lines meet in only one point can be expressed as follows using the assertion symbol.
$\mathrm{assertion}\left(\mathrm{configuration}\left(\mathrm{point}\left(A\right),\mathrm{point}\left(B\right),\mathrm{line}\left(l,\mathrm{incident}\left(A,l\right),\mathrm{incident}\left(B,l\right)\right),\mathrm{line}\left(m,\mathrm{incident}\left(A,m\right),\mathrm{incident}\left(B,m\right),¬\left(l=m\right)\right),A=B\right)\right)$
Signatures:
sts

 [Next: are_on_line] [Previous: type] [Top]

## are_on_line

Description:

The statement that a set of points is collinear.

Example:
This example states that A, B, C, and D are collinear.
$\mathrm{are_on_line}\left(A,B,C,D\right)$
Signatures:
sts

 [First: point] [Previous: assertion] [Top]

 Home Overview Documents Content Dictionaries Software & Tools The OpenMath Society OpenMath Projects OpenMath Discussion Lists OpenMath Meetings Links