Computer assistance for ``discovering'' formulas in system engineering and operator theory (Q1282332)

The objective of this paper is twofold. First the authors present in considerable detail a methodology for using a combination of computer assistance and human intervention to discover highly algebraic theorems in operator, matrix, and linear systems engineering theory. Secondly the authors illustrate the methodology by deriving theorems: 1. The Bart-Gohberg-Kaashoek-van Dooren theorem. 2. An \(H^\infty\) control problem theorem. 3. Matrix completion problems. The commands used in deriving these results rely on noncommutative Gröbner Basis algorithms. The reader need not understand this theoretical basis in order to appreciate the derivation of these theorems. However, in the second part of this paper, theory and more details are given. This part contains background on ideals and Gröbner bases and also more details on the commands used in the first part of this paper.