This paper is one of a series underpinning the authorsʼ DAETS code for solving DAE initial value problems by Taylor series expansion. First, building on the second authorʼs structural analysis of DAEs (BIT, 41 (2001), pp. 364-394), it describes and justifies the method used in DAETS to compute Taylor coefficients (TCs) using automatic differentiation. The DAE may be fully implicit, nonlinear, and contain derivatives of order higher than one. Algorithmic details are given.Second, it proves that either the method succeeds in the sense of computing TCs of the local solution, or one of a number of detectable error conditions occurs.