Feasible Proofs of Matrix Properties with Csanky's Algorithm

Michael Soltys

We show that Csanky's fast parallel algorithm for computing the characteristic polynomial of a matrix can be formalized in the logical theory LAP, and can be proved correct in LAP…