OpenMath Content Dictionary: plangeo1

Canonical URL:

http://www.win.tue.nl/~amc/oz/om/cds/plangeo1.ocd

CD File:

plangeo1.ocd

CD as XML Encoded OpenMath:

plangeo1.omcd

Defines:

configuration, incident, line, point, type

Date:

2002-03-15

Version:

0.1

Review Date:

00

Status:

unofficial

Uses CD:

logic1.ocd, relation1.ocd

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="plangeo1" name="point"/>
    <OMV name="A"/>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="A"/>
      <OMV name="l"/>
    </OMA>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="A"/>
      <OMV name="m"/>
    </OMA>
  </OMA>
</OMOBJ>

point ( A, incident ( A, l) , incident ( A, m) )

$$\mathrm{point}(A,\mathrm{incident}(A,l),\mathrm{incident}(A,m))$$

Signatures:

sts

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="plangeo1" name="line"/>
    <OMV name="l"/>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="A"/>
      <OMV name="l"/>
    </OMA>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="B"/>
      <OMV name="l"/>
    </OMA>
  </OMA>
</OMOBJ>

line ( l, incident ( A, l) , incident ( B, l) )

$$\mathrm{line}(l,\mathrm{incident}(A,l),\mathrm{incident}(B,l))$$

Signatures:

sts

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="plangeo1" name="incident"/>
    <OMV name="A"/>
    <OMV name="l"/>
  </OMA>
</OMOBJ>

incident ( A, l)

$$\mathrm{incident}(A,l)$$

Signatures:

sts

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="plangeo1" name="configuration"/>
    <OMA>
      <OMS cd="plangeo1" name="point"/> 
      <OMV name="A"/>
    </OMA>
    <OMA>
      <OMS cd="plangeo1" name="line"/>
      <OMV name="l"/>
      <OMA>
        <OMS cd="plangeo1" name="incident"/>
        <OMV name="A"/>
        <OMV name="l"/>
      </OMA>
    </OMA>
</OMA>
</OMOBJ>

configuration (point ( A) , line ( l, incident ( A, l) ) )

$$\mathrm{configuration}(\mathrm{point}\left(A\right),\mathrm{line}(l,\mathrm{incident}(A,l)))$$

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="plangeo1" name="configuration"/>
    <OMA>
      <OMS cd="plangeo1" name="configuration"/>
        <OMA>
          <OMS cd="plangeo1" name="point"/> 
          <OMV name="A"/>
        </OMA>
        <OMA>
          <OMS cd="plangeo1" name="line"/>
          <OMV name="l"/>
          <OMA>
            <OMS cd="plangeo1" name="incident"/>
            <OMV name="A"/>
            <OMV name="l"/>
          </OMA>
        </OMA>
     </OMA>
    <OMA>
      <OMS cd="plangeo1" name="point"/>
        <OMV name="B"/>
        <OMA>
          <OMS cd="plangeo1" name="incident"/>
          <OMV name="B"/>
          <OMV name="l"/>
        </OMA>
    </OMA>
</OMA>
</OMOBJ>

configuration (configuration (point ( A) , line ( l, incident ( A, l) ) ) , point ( B, incident ( B, l) ) )

$$\mathrm{configuration}(\mathrm{configuration}(\mathrm{point}\left(A\right),\mathrm{line}(l,\mathrm{incident}(A,l))),\mathrm{point}(B,\mathrm{incident}(B,l)))$$

Example:

We describe a triangle on the distinct points A, B, C and lines a, b, c:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="plangeo1" name="configuration"/>
  <OMA>
    <OMS cd="plangeo1" name="point"/>
    <OMV name="A"/>
  </OMA>
  
  <OMA>
    <OMS cd="plangeo1" name="point"/>
    <OMV name="B"/>
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMV name="A"/>
        <OMV name="B"/>
      </OMA>
    </OMA>
  </OMA>

  <OMA>
    <OMS cd="plangeo1" name="line"/>
    <OMV name="c"/>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="c"/>
      <OMV name="A"/>
    </OMA>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="c"/>
      <OMV name="B"/>
    </OMA>
  </OMA>

  <OMA>
    <OMS cd="plangeo1" name="point"/>
    <OMV name="C"/>
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMA>
        <OMS cd="plangeo1" name="incident"/>
        <OMV name="C"/>
        <OMV name="c"/>
      </OMA>
    </OMA>
  </OMA>

  <OMA>
    <OMS cd="plangeo1" name="line"/>
    <OMV name="a"/>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="a"/>
      <OMV name="B"/>
    </OMA>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="a"/>
      <OMV name="C"/>
    </OMA>
  </OMA>

  <OMA>
    <OMS cd="plangeo1" name="line"/>
    <OMV name="b"/>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="b"/>
      <OMV name="A"/>
    </OMA>
    <OMA>
      <OMS cd="plangeo1" name="incident"/>
      <OMV name="b"/>
      <OMV name="C"/>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

configuration (point ( A) , point ( B, not (eq ( A, B) ) ) , line ( c, incident ( c, A) , incident ( c, B) ) , point ( C, not (incident ( C, c) ) ) , line ( a, incident ( a, B) , incident ( a, C) ) , line ( b, incident ( b, A) , incident ( b, C) ) )

$$\mathrm{configuration}(\mathrm{point}\left(A\right),\mathrm{point}(B,\neg (A=B)),\mathrm{line}(c,\mathrm{incident}(c,A),\mathrm{incident}(c,B)),\mathrm{point}(C,\neg \mathrm{incident}(C,c)),\mathrm{line}(a,\mathrm{incident}(a,B),\mathrm{incident}(a,C)),\mathrm{line}(b,\mathrm{incident}(b,A),\mathrm{incident}(b,C)))$$

Signatures:

sts

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):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
       <OMS cd="relation1" name="eq"/>
       <OMA>
          <OMS cd="plangeo1" name="type"/>
          <OMV name="A"/>
       </OMA>
       <OMA>
          <OMS cd="plangeo1" name="type"/>
          <OMV name="B"/>
       </OMA>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMA>
        <OMS cd="plangeo1" name="incident"/>
        <OMV name="A"/>
        <OMV name="B"/>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>

implies (eq (type ( A) , type ( B) ) , not (incident ( A, B) ) )

$$\mathrm{type}\left(A\right)=\mathrm{type}\left(B\right)\Rightarrow \neg \mathrm{incident}(A,B)$$

Signatures:

sts