Specification and integration of theorem provers and computer algebra systems