(=>
(and
(radius ?CIRCLE ?RADIUS)
(pointOfFigure ?POINT ?CIRCLE))
(exists (?CENTER)
(and
(equal ?CENTER
(CenterOfCircleFn ?CIRCLE))
(geometricDistance ?CENTER ?POINT ?RADIUS)))) |
Merge.kif 7818-7826 |
If the radius of X is Y and Z is a vertex of X, then there exists W such that equal W, the center of circle of X, and W is geometric distance Z for Y |
(=>
(and
(tangent ?LINE ?CIRCLE)
(pointOfFigure ?POINT1 ?LINE)
(pointOfFigure ?POINT1 ?CIRCLE)
(pointOfFigure ?POINT2 ?LINE)
(pointOfFigure ?POINT2 ?CIRCLE))
(equal ?POINT1 ?POINT2)) |
Mid-level-ontology.kif 5411-5418 |
If a tangent of X is Y, Z is a vertex of Y, Z is a vertex of X, W is a vertex of Y, and W is a vertex of X, then equal Z and W |
(=>
(and
(equal
(CenterOfCircleFn ?C) ?P)
(pointOfFigure ?P2 ?C)
(geometricDistance ?P2 ?P ?R))
(equal
(RadiusFn ?C) ?R)) |
Mid-level-ontology.kif 5736-5741 |
If equal the center of circle of X and Y, Z is a vertex of X, and Z is geometric distance Y for W, then equal the radius of X and W |
(=>
(and
(equal ?A CircularArc)
(pointOfFigure ?P ?A))
(exists (?C ?P2)
(and
(geometricPart ?A ?C)
(equal ?C Circle)
(pointOfFigure ?P2 ?C)
(equal ?P ?P2)))) |
Mid-level-ontology.kif 5815-5824 |
If equal X and circular arc and Y is a vertex of X, then All of the following hold: (1) there exist Z (2) W such that Z is a geometric part of X (3) equal Z (4) circle (5) W is a vertex of Z (6) equal Y (7) W |
(=>
(and
(equal ?CHORD ChordOfACircle)
(pointOfFigure
(CenterOfCircleFn ?C) ?CHORD)
(equal ?C Circle))
(equal ?CHORD DiameterLine)) |
Mid-level-ontology.kif 6003-6009 |
If equal X and chord of a circle, the center of circle of Y is a vertex of X, and equal Y and circle, then equal X and diameter line |
(=>
(and
(equal ?S SecantLine)
(pointOfFigure ?P1 ?S)
(pointOfFigure ?P2 ?S)
(not
(equal ?P1 ?P2))
(equal ?C Circle)
(pointOfFigure ?P1 ?C)
(pointOfFigure ?P2 ?C))
(exists (?CHORD)
(and
(equal ?CHORD ChordOfACircle)
(endPointsOfLine ?P1 ?P2 ?CHORD)
(geometricPart ?CHORD ?S)))) |
Mid-level-ontology.kif 6024-6038 |
If All of the following hold: (1) equal X and secant line (2) Y is a vertex of X (3) Z is a vertex of X (4) equal Y and Z (5) equal W and circle (6) Y is a vertex of W (7) Z is a vertex of W, then there exists V such that equal V, chord of a circle, Y, Z are endPointsOfLine of V, and X is a geometric part of V |
(=>
(and
(attribute ?OBJ ?SPHERE)
(pointOfFigure ?PT1 ?OBJ)
(pointOfFigure ?PT2 ?OBJ)
(instance ?SPHERE Sphere))
(exists (?CENTER ?DIST)
(and
(geometricDistance ?PT1 ?CENTER ?DIST)
(geometricDistance ?PT2 ?CENTER ?DIST)))) |
Mid-level-ontology.kif 6084-6093 |
If X is an attribute of Y, Z is a vertex of Y, W is a vertex of Y, and X is an instance of sphere, then there exist V, U such that Z is geometric distance V for U, and W is geometric distance V for U |