Information Technology Reference
In-Depth Information
To prove the above statement we use the Grobner bases method. First we
have to transform the problem into algebraic form.
To transform the geometric problem into an algebraic form we choose an
orthogonal coordinate system.
Let us have the origin in point
A
,andpoints
{
B, M
}
and
{
G, D, I
}
on the
two axes.
Using this coordinate system we have the following points:
{{
A,
0
,
0
}
,
{
B, u
1
,
0
}
,
{
D,
0
,x
1
}
,
{
E, x
2
,u
2
}
,
{
α
G
,
0
,x
3
}
,
{
G,
0
,x
4
}
,
{
α
I
,
0
,x
5
}
,
{
I,
0
,x
6
}
,
{
M, x
7
,
0
}
,
{
C, x
8
,x
9
}
,
{
F, x
10
,x
11
}
,
{
H, x
12
,x
13
}
,
{
L, x
14
,x
15
}
,
{
α
L
,x
16
,x
17
}
,
{
K, x
18
,x
19
}
,
,
where
α
X
is a variable generated internally to create point
X
.
The algebraic form
2
of the given construction is:
{
α
N
,x
20
,x
21
}
,
{
N, x
22
,x
23
}
,
{
α
J
,x
24
,x
25
}
,
{
J, x
26
,x
27
}}
u
1
+
u
1
x
8
== 0
∀
x
0
,...,x
27
((
−
1) +
u
1
x
0
== 0
∧−
u
1
+
−
x
1
== 0
∧−
∧
x
1
+
x
1
x
9
== 0
−
∧−
x
1
x
2
+
−
u
2
x
8
+
x
1
x
8
+
x
2
x
9
== 0
∧
−
x
1
+2
x
3
== 0
∧
x
1
x
3
+
−
x
1
x
4
== 0
∧
−
u
1
x
9
+
x
9
x
10
+
u
1
x
11
+
−
x
8
x
11
== 0
∧
x
1
x
3
+
−
x
1
x
11
== 0
∧−
x
4
+2
x
5
== 0
∧
x
4
x
5
+
−
x
4
x
6
== 0
∧
−
u
1
x
11
+
x
11
x
12
+
u
1
x
13
+
−
x
10
x
13
== 0
∧
x
4
x
5
+
−
x
4
x
13
== 0
∧
−
x
6
x
12
+
x
6
x
14
+
−
x
13
x
14
+
x
12
x
15
== 0
∧−
x
14
+2
x
16
== 0
∧
−
x
15
+2
x
17
== 0
∧−
x
14
x
16
+
−
x
15
x
17
+
x
14
x
18
+
x
15
x
19
== 0
∧
−
x
1
x
8
+
x
1
x
18
+
−
x
9
x
18
+
x
8
x
19
== 0
∧
x
7
x
14
+
−
x
14
x
16
+
−
x
15
x
17
== 0
∧
x
7
x
19
+
−
x
19
x
20
+
−
x
7
x
21
+
x
18
x
21
== 0
∧
−
x
4
x
19
+
−
x
7
x
20
+
x
18
x
20
+
x
19
x
21
== 0
∧
2
x
20
+
−
x
22
== 0
∧
−
x
4
+2
x
21
+
−
x
23
== 0
∧−
u
2
x
22
+
x
2
x
23
== 0
∧
−
x
7
x
19
+
x
19
x
24
+
x
7
x
25
+
−
x
18
x
25
== 0
∧
x
6
x
19
+
x
7
x
24
+
−
x
18
x
24
+
−
x
19
x
25
== 0
∧
2
x
24
+
−
x
26
== 0
∧−
x
6
+2
x
25
+
−
x
27
== 0
⇒
u
2
x
14
x
26
+
−
x
2
x
15
x
26
+
−
x
2
x
14
x
27
+
−
u
2
x
15
x
27
== 0
∧
2
x
14
x
15
x
26
+
x
14
x
27
+
x
15
x
27
== 0)
−
−
The further output of the proof is omitted here; the proof proceeds as outlined
in step (iii).
Namely,
1. The above problem is decomposed into two independent problems.
2. The individual problems are separately proved.
3. For each problem, the reduced Grobner bases are computed.
4. Since the result of the computation is
{
}
1
for each individual problem, the
proposition is generally true.
2
Notation
x
0
, ..., x
27
represents the full sequence of consecutive variables from
x
0
to
x
27
.
Search WWH ::
Custom Search