Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms | Publicación