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:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo1">point</csymbol>
  <ci>A</ci>
  <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply>
  <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>m</ci></apply>
 </apply>
</math>

Prefix

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

Popcorn

plangeo1.point($A, plangeo1.incident($A, $l), plangeo1.incident($A, $m))

Rendered Presentation MathML

$$\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:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo1">line</csymbol>
  <ci>l</ci>
  <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply>
  <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>l</ci></apply>
 </apply>
</math>

Prefix

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

Popcorn

plangeo1.line($l, plangeo1.incident($A, $l), plangeo1.incident($B, $l))

Rendered Presentation MathML

$$\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:

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply></math>

Prefix

incident ( A, l)

Popcorn

plangeo1.incident($A, $l)

Rendered Presentation MathML

$$\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:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo1">configuration</csymbol>
  <apply><csymbol cd="plangeo1">point</csymbol><ci>A</ci></apply>
  <apply><csymbol cd="plangeo1">line</csymbol>
   <ci>l</ci>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

plangeo1.configuration(plangeo1.point($A), plangeo1.line($l, plangeo1.incident($A, $l)))

Rendered Presentation MathML

$$\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:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo1">configuration</csymbol>
  <apply><csymbol cd="plangeo1">configuration</csymbol>
   <apply><csymbol cd="plangeo1">point</csymbol><ci>A</ci></apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>l</ci>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply>
   </apply>
  </apply>
  <apply><csymbol cd="plangeo1">point</csymbol>
   <ci>B</ci>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>l</ci></apply>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

plangeo1.configuration(plangeo1.configuration(plangeo1.point($A), plangeo1.line($l, plangeo1.incident($A, $l))), plangeo1.point($B, plangeo1.incident($B, $l)))

Rendered Presentation MathML

$$\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:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo1">configuration</csymbol>
  <apply><csymbol cd="plangeo1">point</csymbol><ci>A</ci></apply>
  <apply><csymbol cd="plangeo1">point</csymbol>
   <ci>B</ci>
   <apply><csymbol cd="logic1">not</csymbol>
    <apply><csymbol cd="relation1">eq</csymbol><ci>A</ci><ci>B</ci></apply>
   </apply>
  </apply>
  <apply><csymbol cd="plangeo1">line</csymbol>
   <ci>c</ci>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>A</ci></apply>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>B</ci></apply>
  </apply>
  <apply><csymbol cd="plangeo1">point</csymbol>
   <ci>C</ci>
   <apply><csymbol cd="logic1">not</csymbol>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>C</ci><ci>c</ci></apply>
   </apply>
  </apply>
  <apply><csymbol cd="plangeo1">line</csymbol>
   <ci>a</ci>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>B</ci></apply>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>C</ci></apply>
  </apply>
  <apply><csymbol cd="plangeo1">line</csymbol>
   <ci>b</ci>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>A</ci></apply>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>C</ci></apply>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

plangeo1.configuration(plangeo1.point($A), plangeo1.point($B, not($A = $B)), plangeo1.line($c, plangeo1.incident($c, $A), plangeo1.incident($c, $B)), plangeo1.point($C, not(plangeo1.incident($C, $c))), plangeo1.line($a, plangeo1.incident($a, $B), plangeo1.incident($a, $C)), plangeo1.line($b, plangeo1.incident($b, $A), plangeo1.incident($b, $C)))

Rendered Presentation MathML

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

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="plangeo1">type</csymbol><ci>A</ci></apply>
   <apply><csymbol cd="plangeo1">type</csymbol><ci>B</ci></apply>
  </apply>
  <apply><csymbol cd="logic1">not</csymbol>
   <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>B</ci></apply>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

plangeo1.type($A) = plangeo1.type($B) ==> not(plangeo1.incident($A, $B))

Rendered Presentation MathML

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

Signatures:

sts

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.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="plangeo1" name="assertion"/>
     <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>
          <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>
          <OMA><OMS cd="plangeo1" name="line"/>
               <OMV name="m"/>
               <OMA><OMS cd="plangeo1" name="incident"/>
                    <OMV name="A"/>
                    <OMV name="m"/>
               </OMA>
               <OMA><OMS cd="plangeo1" name="incident"/>
                    <OMV name="B"/>
                    <OMV name="m"/>
               </OMA>
               <OMA><OMS cd="logic1" name="not"/>
                    <OMA><OMS cd="relation1" name="eq"/>
                         <OMV name="l"/>
                         <OMV name="m"/>
                    </OMA>
               </OMA>
          </OMA>
          <OMA><OMS cd="relation1" name="eq"/>
               <OMV name="A"/>
               <OMV name="B"/>
          </OMA>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo1">assertion</csymbol>
  <apply><csymbol cd="plangeo1">configuration</csymbol>
   <apply><csymbol cd="plangeo1">point</csymbol><ci>A</ci></apply>
   <apply><csymbol cd="plangeo1">point</csymbol><ci>B</ci></apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>l</ci>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>l</ci></apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>m</ci>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>m</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>m</ci></apply>
    <apply><csymbol cd="logic1">not</csymbol>
     <apply><csymbol cd="relation1">eq</csymbol><ci>l</ci><ci>m</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="relation1">eq</csymbol><ci>A</ci><ci>B</ci></apply>
  </apply>
 </apply>
</math>

Prefix

assertion (configuration (point ( A) , point ( B) , line ( l, incident ( A, l) , incident ( B, l) ) , line ( m, incident ( A, m) , incident ( B, m) , not (eq ( l, m) ) ) , eq ( A, B) ) )

Popcorn

plangeo1.assertion(plangeo1.configuration(plangeo1.point($A), plangeo1.point($B), plangeo1.line($l, plangeo1.incident($A, $l), plangeo1.incident($B, $l)), plangeo1.line($m, plangeo1.incident($A, $m), plangeo1.incident($B, $m), not($l = $m)), $A = $B))

Rendered Presentation MathML

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

Signatures:

sts

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.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA>
  <OMS cd="plangeo1" name="are_on_line"/>
  <OMV name="A"/>
  <OMV name="B"/>
  <OMV name="C"/>
  <OMV name="D"/>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo1">are_on_line</csymbol>
  <ci>A</ci>
  <ci>B</ci>
  <ci>C</ci>
  <ci>D</ci>
 </apply>
</math>

Prefix

are_on_line ( A, B, C, D)

Popcorn

plangeo1.are_on_line($A, $B, $C, $D)

Rendered Presentation MathML

$$\mathrm{are\_on\_line}(A,B,C,D)$$

Signatures:

sts