The paper considers the analysis technique of the general and individual properties of aggregative specifications. The method is based on constructing a set of axioms describing both the aggregate specifications and the properties of the model under investigation. The resolution method using logical programming language PROLOG is applied in creating the axiom system. An example of aggregative specification analysis for the alternating bit protocol is presented.