The logic languages of the TPTP world
Geoff Sutcliffe
Abstract
Abstract The Thousands of Problems for Theorem Provers (TPTP) World is a well-established infrastructure that supports research, development and deployment of automated theorem proving systems. This paper provides an overview of the logic languages of the TPTP World, from classical first-order form (FOF), through typed FOF, up to typed higher-order form, and beyond to non-classical forms. The logic languages are described in a non-technical way and are illustrated with examples using the TPTP language.
Topics & Concepts
Computer scienceAutomated theorem provingProgramming languageFirst-order logicAutomated reasoningLogic, programming, and type systemsLogic, Reasoning, and KnowledgeFormal Methods in Verification