Next: Formal descriptions of
Up: Theory and more details
Suppose you are working with matrices a, b, c etc. If an NCProcess
command discovers that ab = bc and, at that point, you realize that
it is reasonable to assume that no eigenvalue of a is an eigenvalue
of c, then b must be zero from an anlytic argument
Therefore, one can add the polynomial equation b = 0 to the
collection of polynomial equations and contunue. As research
progressed, one would add more and more analytic observations at the
pooints where it became clear what those observations were.
The syllogism corresponding to the above type of argument
would go as follows.
If < whatever hypothesis >, then ab = bc.
If a, b and c are matrices, no eigenvalue of a is an eigenvalue of c
and ab = bc, then b = 0.
If < whatever hypothsis > and b = 0, then < desired
If < whatever hypothesis >, then < desired conclusion
Fact B.2 would be seen by using the algorithms in
this paper. Fact B.3
is an observation from analysis.
Fact B.4 would be seen by using the
algorithms in this paper.
is a tautological conclusion of the
Facts B.2, B.3 and B.4.
Wed Jul 3 10:27:42 PDT 1996