Clustering method and its formalization

Clustering method is an important research technology in data mining, and it has a widely use in our life. This paper will describe some traditional algorithms according to different clustering classification, and point out their advantages and shortcomings. Meanwhile, this paper will summarize the concept of formalization, and introduce several common formal specification languages. After applying the predicate logic language with the real example, we can describe the traditional clustering algorithms like k-means, validate the correctness of method itself, and provide a new research idea for algorithms' examination and innovation.