The TPTP Format for Interpretations
Provides a common format for interpretations in automated reasoning, benefiting the theorem proving community by enabling model sharing and verification.
This paper presents a standardized TPTP format for representing interpretations (Tarskian, Herbrand, Kripke), detailing its syntax, semantics, and verification, with examples and tool support.
This paper describes the TPTP format for representing interpretations. It provides a background survey that helped 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 format are expounded in detail, with multiple examples. Verification of models is discussed. Some tools that support processing the format are noted. The properties of interpretations represented in the format are discussed.