Formalizing Pfaffian in bounded arithmetic

Satoru Kuroda

We formalize algorithms computing Pfaffian in the theory of bounded arithmetic for sharpL which is based on Berkowitz algorithm for the determinant. We also prove relations among P…