OpenMath Content Dictionary: plangeo4

Canonical URL:

http://www.openmath.org/cd/plangeo4.ocd

CD Base:

http://www.openmath.org/cd

CD File:

plangeo4.ocd

CD as XML Encoded OpenMath:

plangeo4.omcd

Defines:

affine_coordinates, set_affine_coordinates, coordinates, is_affine, set_coordinates

Date:

2004-06-01

Version:

0 (Revision 5)

Review Date:

2006-06-01

Status:

experimental

This CD defines symbols for planar Euclidean geometry. In particular, it is concerned with projective and affine coordinates of points and lines.

set_coordinates

Description:

This symbol defines the coordinates of a point or a line. The coordinates are the projective coordinates and consist of a vector of length 3. Points whose third coordinates are zero are the points at infinity. The line whose first two coordinates are zero is the line at infinity.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMBIND>
<OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="v"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="A"/>
      </OMBVAR>
      <OMA>
        <OMS cd="plangeo4" name="set_coordinates"/>
        <OMV name="A"/>
        <OMV name="v"/>
      </OMA>
    </OMBIND>   
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>1</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>2</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>3</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>v</ci></bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <bind><csymbol cd="quant1">exists</csymbol>
    <bvar><ci>A</ci></bvar>
    <apply><csymbol cd="plangeo4">set_coordinates</csymbol><ci>A</ci><ci>v</ci></apply>
   </bind>
   <apply><csymbol cd="logic1">not</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>1</cn><ci>v</ci></apply>
      <csymbol cd="alg1">zero</csymbol>
     </apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>2</cn><ci>v</ci></apply>
      <csymbol cd="alg1">zero</csymbol>
     </apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>3</cn><ci>v</ci></apply>
      <csymbol cd="alg1">zero</csymbol>
     </apply>
    </apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

forall [ v ] . (implies (exists [ A ] . (set_coordinates ( A, v) ) , not (and (eq (vector_selector (1, v) , zero) , eq (vector_selector (2, v) , zero) , eq (vector_selector (3, v) , zero) ) ) ) )

Popcorn

quant1.forall[$v -> quant1.exists[$A -> plangeo4.set_coordinates($A, $v)] ==> not(linalg1.vector_selector(1, $v) = alg1.zero and linalg1.vector_selector(2, $v) = alg1.zero and linalg1.vector_selector(3, $v) = alg1.zero)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}v.\exists \hspace{0.17em}A.\mathrm{set\_coordinates}(A,v)\Rightarrow \neg (v_1=0\wedge v_2=0\wedge v_3=0)$$

Signatures:

sts

coordinates

Description:

This function yields the coordinates vector if applied to a point or line with coordinates.

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="logic1" name="and"/>
    <OMA>
     <OMS cd="relation1" name="eq"/>
     <OMV name="v"/>
     <OMA>
       <OMS cd="plangeo4" name="coordinates"/>
       <OMA>
         <OMS cd="plangeo1" name="point"/>
         <OMV name="A"/>
       </OMA>
     </OMA>
    <OMA>
     <OMS cd="relation1" name="eq"/>
     <OMV name="w"/>
     <OMA>
       <OMS cd="plangeo4" name="coordinates"/>
       <OMA>
         <OMS cd="plangeo1" name="line"/>
         <OMV name="L"/>
       </OMA>
     </OMA>
    </OMA>
  </OMA> 
  <OMA>
   <OMS cd="relation1" name="eq"/>
   <OMA>
     <OMS cd="arith1" name="plus"/>
     <OMA>
       <OMS cd="arith1" name="times"/>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>1</OMI>
         <OMV name="v"/>
       </OMA>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>1</OMI>
         <OMV name="w"/>
       </OMA>
     </OMA>
     <OMA>
       <OMS cd="arith1" name="times"/>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>2</OMI>
         <OMV name="v"/>
       </OMA>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>2</OMI>
         <OMV name="w"/>
       </OMA>
     </OMA>
     <OMA>
       <OMS cd="arith1" name="times"/>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>3</OMI>
         <OMV name="v"/>
       </OMA>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>3</OMI>
         <OMV name="w"/>
       </OMA>
     </OMA>
    </OMA>
    <OMS cd="alg1" name="zero"/>
  </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="logic1">and</csymbol>
   <apply><csymbol cd="relation1">eq</csymbol>
    <ci>v</ci>
    <apply><csymbol cd="plangeo4">coordinates</csymbol>
     <apply><csymbol cd="plangeo1">point</csymbol><ci>A</ci></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <ci>w</ci>
     <apply><csymbol cd="plangeo4">coordinates</csymbol>
      <apply><csymbol cd="plangeo1">line</csymbol><ci>L</ci></apply>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply><csymbol cd="arith1">plus</csymbol>
     <apply><csymbol cd="arith1">times</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>1</cn><ci>v</ci></apply>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>1</cn><ci>w</ci></apply>
     </apply>
     <apply><csymbol cd="arith1">times</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>2</cn><ci>v</ci></apply>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>2</cn><ci>w</ci></apply>
     </apply>
     <apply><csymbol cd="arith1">times</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>3</cn><ci>v</ci></apply>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>3</cn><ci>w</ci></apply>
     </apply>
    </apply>
    <csymbol cd="alg1">zero</csymbol>
   </apply>
  </apply>
 </apply>
</math>

Prefix

implies (and (eq ( v, coordinates (point ( A) ) , eq ( w, coordinates (line ( L) ) ) ) , eq (plus (times (vector_selector (1, v) , vector_selector (1, w) ) , times (vector_selector (2, v) , vector_selector (2, w) ) , times (vector_selector (3, v) , vector_selector (3, w) ) ) , zero) ) )

Popcorn

$v = plangeo4.coordinates(plangeo1.point($A)) = $w = plangeo4.coordinates(plangeo1.line($L)) and linalg1.vector_selector(1, $v) * linalg1.vector_selector(1, $w) + linalg1.vector_selector(2, $v) * linalg1.vector_selector(2, $w) + linalg1.vector_selector(3, $v) * linalg1.vector_selector(3, $w) = alg1.zero

Rendered Presentation MathML

$$v=\mathrm{coordinates}\left(\mathrm{point}\left(A\right)\right)=w=\mathrm{coordinates}\left(\mathrm{line}\left(L\right)\right)\wedge v_1{w}_1+v_2{w}_2+v_3{w}_3=0\Rightarrow$$

Example:

To extract the coordinates of a point A with coordinates (1,2,3):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0"> 
<OMA>
   <OMS cd="plangeo4" name="coordinates"/> 
   <OMA>
     <OMS cd="plangeo1" name="point"/>
     <OMV name="A"/>
     <OMA>
       <OMS cd="plangeo4" name="set_coordinates"/>
       <OMV name="A"/>
       <OMA>
         <OMS cd="linalg2" name="vector"/>
         <OMI>1</OMI>
         <OMI>2</OMI>
         <OMI>3</OMI>
       </OMA>
     </OMA>
   </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo4">coordinates</csymbol>
  <apply><csymbol cd="plangeo1">point</csymbol>
   <ci>A</ci>
   <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
    <ci>A</ci>
    <apply><csymbol cd="linalg2">vector</csymbol><cn>1</cn><cn>2</cn><cn>3</cn></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

coordinates (point ( A, set_coordinates ( A, vector (1, 2, 3) ) ) )

Popcorn

plangeo4.coordinates(plangeo1.point($A, plangeo4.set_coordinates($A, linalg2.vector(1, 2, 3))))

Rendered Presentation MathML

$$\mathrm{coordinates}\left(\mathrm{point}(A,\mathrm{set\_coordinates}(A,(1,2,3)))\right)$$

Signatures:

sts

is_affine

Description:

Boolean function testing whether a point or line is affine.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMBIND><OMS cd="quant1" name="forall"/>
     <OMBVAR><OMV name="v"/></OMBVAR>
     <OMA><OMS cd="logic1" name="implies"/>
          <OMBIND><OMS cd="quant1" name="exists"/>
               <OMBVAR><OMV name="A"/></OMBVAR>
               <OMA><OMS cd="plangeo1" name="point"/>
                    <OMV name="A"/>
                    <OMA><OMS cd="plangeo4" name="set_coordinates"/>
                         <OMV name="A"/><OMV name="v"/>
                    </OMA>
                    <OMA><OMS cd="plangeo4" name="is_affine"/>
                         <OMV name="A"/>
                    </OMA>
               </OMA>
          </OMBIND>   
          <OMA><OMS cd="logic1" name="not"/>
               <OMA><OMS cd="relation1" name="eq"/>
                    <OMA><OMS cd="linalg1" name="vector_selector"/>
                         <OMI>3</OMI>  <OMV name="v"/>
                    </OMA>
                    <OMS cd="alg1" name="zero"/>
               </OMA>
          </OMA>
     </OMA>
</OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>v</ci></bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <bind><csymbol cd="quant1">exists</csymbol>
    <bvar><ci>A</ci></bvar>
    <apply><csymbol cd="plangeo1">point</csymbol>
     <ci>A</ci>
     <apply><csymbol cd="plangeo4">set_coordinates</csymbol><ci>A</ci><ci>v</ci></apply>
     <apply><csymbol cd="plangeo4">is_affine</csymbol><ci>A</ci></apply>
    </apply>
   </bind>
   <apply><csymbol cd="logic1">not</csymbol>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>3</cn><ci>v</ci></apply>
     <csymbol cd="alg1">zero</csymbol>
    </apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

forall [ v] . (implies (exists [ A] . (point ( A, set_coordinates ( A, v) , is_affine ( A) ) ) , not (eq (vector_selector (3, v) , zero) ) ) )

Popcorn

quant1.forall[$v -> quant1.exists[$A -> plangeo1.point($A, plangeo4.set_coordinates($A, $v), plangeo4.is_affine($A))] ==> not(linalg1.vector_selector(3, $v) = alg1.zero)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}v.\exists \hspace{0.17em}A.\mathrm{point}(A,\mathrm{set\_coordinates}(A,v),\mathrm{is\_affine}\left(A\right))\Rightarrow \neg (v_3=0)$$

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMBIND>
<OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="v"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR><OMV name="A"/></OMBVAR>
        <OMA>
          <OMS cd="plangeo1" name="line"/>
          <OMV name="A"/>
          <OMA>
            <OMS cd="plangeo4" name="set_coordinates"/>
            <OMV name="A"/>
            <OMV name="v"/>
          </OMA>
          <OMA>
            <OMS cd="plangeo4" name="is_affine"/>
            <OMV name="A"/>
          </OMA>
        </OMA>
    </OMBIND>   
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>1</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>2</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>v</ci></bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <bind><csymbol cd="quant1">exists</csymbol>
    <bvar><ci>A</ci></bvar>
    <apply><csymbol cd="plangeo1">line</csymbol>
     <ci>A</ci>
     <apply><csymbol cd="plangeo4">set_coordinates</csymbol><ci>A</ci><ci>v</ci></apply>
     <apply><csymbol cd="plangeo4">is_affine</csymbol><ci>A</ci></apply>
    </apply>
   </bind>
   <apply><csymbol cd="logic1">not</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>1</cn><ci>v</ci></apply>
      <csymbol cd="alg1">zero</csymbol>
     </apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="linalg1">vector_selector</csymbol><cn>2</cn><ci>v</ci></apply>
      <csymbol cd="alg1">zero</csymbol>
     </apply>
    </apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

forall [ v ] . (implies (exists [ A] . (line ( A, set_coordinates ( A, v) , is_affine ( A) ) ) , not (and (eq (vector_selector (1, v) , zero) , eq (vector_selector (2, v) , zero) ) ) ) )

Popcorn

quant1.forall[$v -> quant1.exists[$A -> plangeo1.line($A, plangeo4.set_coordinates($A, $v), plangeo4.is_affine($A))] ==> not(linalg1.vector_selector(1, $v) = alg1.zero and linalg1.vector_selector(2, $v) = alg1.zero)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}v.\exists \hspace{0.17em}A.\mathrm{line}(A,\mathrm{set\_coordinates}(A,v),\mathrm{is\_affine}\left(A\right))\Rightarrow \neg (v_1=0\wedge v_2=0)$$

Example:

OpenMath XML (source)

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

Strict Content MathML

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

Prefix

is_affine ( A)

Popcorn

plangeo4.is_affine($A)

Rendered Presentation MathML

$$\mathrm{is\_affine}\left(A\right)$$

Signatures:

sts

affine_coordinates

Description:

This function yields the affine coordinates vector if applied to a point or line with coordinates in the affine plane.

Example:

The affine coordinates (1/3,2/3) are expressed as follows for the point A with projective coordinates (1,2,3).

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA>
  <OMS cd="plangeo4" name="affine_coordinates"/>
   <OMA>
     <OMS cd="plangeo1" name="point"/>
     <OMV name="A"/>
     <OMA>
       <OMS cd="plangeo4" name="set_coordinates"/>
       <OMV name="A"/>
       <OMA>
         <OMS cd="linalg2" name="vector"/>
         <OMI>1</OMI>
         <OMI>2</OMI>
         <OMI>3</OMI>
       </OMA>
     </OMA>
   </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo4">affine_coordinates</csymbol>
  <apply><csymbol cd="plangeo1">point</csymbol>
   <ci>A</ci>
   <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
    <ci>A</ci>
    <apply><csymbol cd="linalg2">vector</csymbol><cn>1</cn><cn>2</cn><cn>3</cn></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

affine_coordinates (point ( A, set_coordinates ( A, vector (1, 2, 3) ) ) )

Popcorn

plangeo4.affine_coordinates(plangeo1.point($A, plangeo4.set_coordinates($A, linalg2.vector(1, 2, 3))))

Rendered Presentation MathML

$$\mathrm{affine\_coordinates}\left(\mathrm{point}(A,\mathrm{set\_coordinates}(A,(1,2,3)))\right)$$

Signatures:

sts

set_affine_coordinates

Description:

Defines the affine coordinates of an affine point or line.

Example:

Assign the affine coordinates (1/3,2/3) to A.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA>
  <OMS cd="plangeo4" name="set_affine_coordinates"/>
  <OMV name="A"/>
     <OMA>
       <OMS cd="linalg2" name="vector"/>
       <OMA>
         <OMS cd="nums1" name="rational"/>
         <OMI> 1 </OMI>
         <OMI> 3 </OMI>
       </OMA>
       <OMA>
         <OMS cd="nums1" name="rational"/>
         <OMI> 2 </OMI>
         <OMI> 3 </OMI>
       </OMA>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
  <ci>A</ci>
  <apply><csymbol cd="linalg2">vector</csymbol>
   <apply><csymbol cd="nums1">rational</csymbol><cn>1</cn><cn>3</cn></apply>
   <apply><csymbol cd="nums1">rational</csymbol><cn>2</cn><cn>3</cn></apply>
  </apply>
 </apply>
</math>

Prefix

set_affine_coordinates ( A, vector (rational ( 1 , 3 ) , rational ( 2 , 3 ) ) )

Popcorn

plangeo4.set_affine_coordinates($A, linalg2.vector(1 // 3, 2 // 3))

Rendered Presentation MathML

$$\mathrm{set\_affine\_coordinates}(A,(\frac{1}{3},\frac{2}{3}))$$

Signatures:

sts