The New TPTP Format for Interpretations

TL;DR

This paper introduces a new TPTP format for representing various types of logical interpretations, detailing its syntax, semantics, and supporting tools, to enhance model verification and application support.

Contribution

It presents a comprehensive new format for interpretations in TPTP, including syntax, semantics, and tool support, tailored for different interpretation types.

Findings

The new format effectively represents Tarskian, Herbrand, and Kripke interpretations.

Tools supporting the new format are identified and discussed.

The format facilitates model verification and application integration.

Abstract

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.