Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The New TPTP Format for Interpretations

Geoff Sutcliffe, Alexander Steen, Pascal Fontaine

TL;DR

The paper introduces a comprehensive new TPTP format for representing interpretations, addressing Tarskian, Herbrand, and Kripke semantics to support explicit model outputs in automated theorem proving. It defines interpretation-formulae as an extension of problem language, provides concrete encoding rules for FOF, TFF, and THF, and describes splitting and compaction techniques to improve modularity and scalability. The approach supports Herbrand saturations and Kripke worlds, with verification workflows that reduce model checking to theorem proving and dedicated tools such as the AGMV model verifier. The framework aims to enhance evaluability, verifiability, and comprehensibility of models, enabling robust analysis, debugging, and validation in ATP applications. The authors outline practical guidance for adoption and future work to extend non-classical logics and broader tool support.

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.

The New TPTP Format for Interpretations

TL;DR

The paper introduces a comprehensive new TPTP format for representing interpretations, addressing Tarskian, Herbrand, and Kripke semantics to support explicit model outputs in automated theorem proving. It defines interpretation-formulae as an extension of problem language, provides concrete encoding rules for FOF, TFF, and THF, and describes splitting and compaction techniques to improve modularity and scalability. The approach supports Herbrand saturations and Kripke worlds, with verification workflows that reduce model checking to theorem proving and dedicated tools such as the AGMV model verifier. The framework aims to enhance evaluability, verifiability, and comprehensibility of models, enabling robust analysis, debugging, and validation in ATP applications. The authors outline practical guidance for adoption and future work to extend non-classical logics and broader tool support.

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.
Paper Structure (59 sections, 1 figure)

This paper contains 59 sections, 1 figure.

Table of Contents

  1. Introduction
  2. Related work:
  3. This paper is organized as follows:
  4. About Interpretations
  5. What do we Need?
  6. What do we Have?
  7. Do we Have what we Need?
  8. Model Verification
  9. The New Format for Tarskian Interpretations
  10. FOF Tarskian Interpretations
  11. TFF and THF Tarskian Interpretations
  12. Examples:
  13. Tarskian Interpretations Split over Multiple Formulae
  14. Tarskian Interpretations Compacted using Quantification
  15. Herbrand-formulae and Saturations
  16. ...and 44 more sections

Figures (1)

  • Figure 1: A Landscape of Model Building