TPTP World Standards and Tools for
Tarskian and Kripke Interpretations

Abstract

This talk describes the (new) TPTP World format for representing Tarskian and Kripke interpretations of formulae in classical (FOF, TFF, TXF, THF) and non-classical (NXF, NHF) logics. A technique and implemented tool for verifying models, and a tool for visualizing Tarskian interpretations, are presented. This work provides TPTP World standards that allow interpretations to be shared between components of complex compositional reasoning systems.