Information Technology Reference
In-Depth Information
a
and
b
be the lengths of the perpendicular sides of the right triangle
ABC
,
c
the length of its hypotenuse, and
B
the angle opposite to side
b
. Then, by
the definition of the trigonometric functions, sin
(
B
)
=
b
/
c
and cos
(
B
)
=
a
/
c
.
From the fundamental trigonometric identity we have: sin
2
cos
2
(
B
)
+
(
B
)
=
c
2
.
The problem with this “proof”, as mentioned above, is that the derivation of
the fundamental trigonometric identity is based on the geometrical fact that the
Pythagorean Theorem expresses; thus this is an example of a circular proof. The
“proof validation” codelets of the system should “perceive” that the same fact is
expressed in both geometric and trigonometric languages and spot this circularity;
but rather than simply rejecting the proof, they could spawn further codelets asking
for a derivation of the trigonometric identity without the use of the Pythagorean
Theorem. Indeed, as pointed out in [
1
], it is possible to derive the trigonometric
identity using solely the subtraction formulas for sine and cosine:
2
2
1, from which we get:
a
2
b
2
1. Consequently,
(
b
/
c
)
+
(
a
/
c
)
=
+
=
sin
(
a
−
b
)
=
sin
(
a
)
cos
(
b
)
−
cos
(
a
)
sin
(
b
)
cos
(
a
−
b
)
=
cos
(
a
)
cos
(
b
)
−
sin
(
a
)
sin
(
b
)
This derivation establishes also that the mathematical fact proven is independent
of the language (style) used in the proof, being it geometric or trigonometric. This
terminates the proof-event under consideration.
4. Finally,
could be asked to take an algebraic approach, which is exhaus-
tive and thus suitable for a computerized system. The choice of algebraic language
makes possible the use of algebraic identities standing for geometric relations.
Specifically, consider Fig.
18.5
(proof #56 in [
1
]):
Assuming the usual assignments
AB
A
4
,
PT
4
=
c
,
AC
=
b
,
BC
=
a
, and further:
CD
=
x
,
CE
=
y
,
AF
=
z
,
EF
=
v
, and
ED
=
w
, the following relations
hold:
1
.
b
(
b
+
x
)
=
cz
10
.
zw
=
y
(
b
+
x
)
2
.
b
(
v
+
w
)
=
az
11
.
xz
=
y
(
v
+
w
)
3
.
c
(
v
+
w
)
=
a
(
b
+
x
)
12
.
x
(
b
+
x
)
=
w
(
v
+
w
)
4
.
bw
=
cy
13
.
z
(
a
−
y
)
=
v
(
b
+
x
)
5
.
bx
=
ay
14
.
z
(
c
−
z
)
=
v
(
v
+
w
)
6
.
cx
=
aw
15
.(
c
−
z
)(
b
+
x
)
=
(
a
−
y
)(
v
+
w
)
7
.
b
(
a
−
y
)
=
cv
16
.
y
(
a
−
y
)
=
vw
8
.
b
(
c
−
z
)
=
av
17
.
y
(
c
−
z
)
=
vx
9
.
c
(
c
−
z
)
=
a
(
a
−
y
)
18
.
w
(
c
−
z
)
=
x
(
a
−
y
)
The purpose is to find combinations of the above equations from which
x
v
,
and
w
can be eliminated, thus leaving a relation that holds between
a
,
b
, and
c
. Clearly, no single equation suffices for this task. A brief examination shows
that no pair of equations suffices, either. Thus, equations must be examined in
sets of three, four, or more. In addition, such sets must contain only independent
equations; for example, Eqs. 1, 2, and 3 comprise a dependent set; so do Eqs. 1,
4, and 10; and so on.
,
y
,
z
,
Search WWH ::
Custom Search