This paper describes the new TPTP format for representing interpretations. It provides a background survey that helped us ensure that the representation format is adequate for different types of interpretations: Tarskian, Herbrand, and Kripke interpretations. The needs of applications that use models are considered. The syntax and semantics of the new format is expounded in detail, with multiple examples. Verification of models is discussed. Some tools that support processing the new format are noted. The properties of interpretations represented in the new format are discussed.

翻译：本文阐述了用于表示解释的新型TPTP格式。通过背景调研确保该表示格式适用于多种解释类型：塔斯基解释、赫布兰德解释与克里普克解释。研究同时考虑了模型应用场景的实际需求。文中通过多个示例详细阐释了新格式的语法与语义，探讨了模型验证方法，列举了支持新格式处理的相关工具，并分析了新格式所表示解释的数学性质。