Next: Formal descriptions of Up: Theory and more details Previous: Adjoints

# Example of discovering

Example B.1 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.

Fact B.2 If < whatever hypothesis >, then ab = bc.

Fact B.3 If a, b and c are matrices, no eigenvalue of a is an eigenvalue of c and ab = bc, then b = 0.

Fact B.4 If < whatever hypothsis > and b = 0, then < desired conclusion >.

Conclusion B.5 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. Conclusion B.5 is a tautological conclusion of the Facts B.2, B.3 and B.4.

Helton
Wed Jul 3 10:27:42 PDT 1996