Abstract: Unified abstraction modeling framework and the formal representation help to realize automated reasoning. With the rapid development of the Internet of Things (IoT), various smart or intelligent objects are embedded in the physical world which partly changes the characters of the composed entities. Our familiar world is accordingly changing into an intelligent world which greatly increases the modeling and reasoning complexity. In this paper, based on the unified knowledge reformulation and abstraction (KRA) model framework presented by Saitta and Zucker, we propose a distinguishable knowledge reformulation and abstraction (dKRA) model according to the characters of the intelligent world. Different from the KRA model which represents the intelligent world in a unified way, the proposed dKRA model can be formalized through three interrelated sub-models and their relationships. We give some definitions and theorems based on the correlative concepts of model-based diagnosis to show that the diagnosis process can be limited in one (or more than one) of the sub-models. By focusing on the model verification during the phase of system designing, the presented diagnosis algorithm running on the dKRA model of an intelligent world is analyzed from both theoretical and experimental perspectives to show the improvement on the diagnosis process running directly on the KRA model of the same intelligent world.