# $Id: tpoint.n3,v 1.12 2002/08/02 16:38:14 jderoo Exp $

# given a circle with center x0, y0 and radius r
# given a line going through a point x1, y1
# what are the tangent points x, y
#
# some mathematical formula conventions
#   [ :sum a, b, ...]     --> a + b + ...
#   [ :product a, b, ...] --> a * b * ...
#   [ :minus a]           --> -a
#   [ :slash a]           --> 1/a
#   [ :square a]          --> a**2
#   [ :sqrt a]            --> a**1/2

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix owl: <http://www.w3.org/2001/10/daml+oil#> .
@prefix : <tpoint#> .

:sum a owl:UnambiguousProperty .
:product a owl:UnambiguousProperty .
:minus a owl:UnambiguousProperty .
:slash a owl:UnambiguousProperty .
:square a owl:UnambiguousProperty .
:sqrt a owl:UnambiguousProperty .

this log:forAll :x0, :y0, :x1, :y1, :r, :m.

{ :rule1 . ([:center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]]) a :Measurement}
  log:implies
 {([ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]; :slope [ :product
    [ :sum [ :minus [ :product :2, :x1, [ :sum :y1, [ :minus :y0]]]],
      [ :sqrt [ :sum [ :product :4, [ :square :x1], [ :square [ :sum :y1, [ :minus :y0]]]],
        [ :minus [ :product :4, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]],
          [ :sum [ :square :r], [ :minus [ :square [ :sum :y0, :y1]]],
            [ :product :2, :y0, [ :sum :x0, [ :minus :y1]]]]]]]]],
    [ :slash [ :product :2, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]]]]]]) a :Calculation} .

{ :rule2 . ([:center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]]) a :Measurement}
  log:implies
 {([ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]; :slope [ :product
    [ :sum [ :minus [ :product :2, :x1, [ :sum :y1, [ :minus :y0]]]],
      [ :minus [ :sqrt [ :sum [ :product :4, [ :square :x1], [ :square [ :sum :y1, [ :minus :y0]]]],
        [ :minus [ :product :4, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]],
          [ :sum [ :square :r], [ :minus [ :square [ :sum :y0, :y1]]],
            [ :product :2, :y0, [ :sum :x0, [ :minus :y1]]]]]]]]]],
    [ :slash [ :product :2, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]]]]]]) a :Calculation} .

{ :rule3 . ([ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]; :slope :m]) a :Calculation}
  log:implies
 {([ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]; :tpoint
    [ :X [ :product [ :sum [ :product [ :square :m], :x1], [ :minus [ :product :m, :y1]], :x0, [ :product :m, :y0]],
      [ :slash [ :sum [ :square :m], :1]]];
      :Y [ :product [ :sum [ :product :m, :x0], [ :product [ :square :m], :y0], [ :minus [ :product :m, :x1]], :y1],
      [ :slash [ :sum [ :square :m], :1]]]]]) a :Calculation} .