How to handle the semantics of the TPTP THF0 language?

Christoph Benzmueller

In an ongoing project (funded by the EU IIF grant THFTPTP 219982) a TPTP infrastructure for typed higher order logic is being developed. As a starting point the THF0 language format has been defined. THF0 covers Church's simple type theory which forms the core logic of choice of many higher order automated theorem provers and proof assistants including the systems TPS, LEO-II, Isabelle/HOL, PVS, HOL4, and OMEGA. Currently a library of proof problems encoded in THF0 is built-up which will be used in the future for the organization of higher order CASC events. There are clearly many further applications of the new higher order TPTP infrastructure. In particular, it is intended to provide a standard interface for connecting higher order proof assistants with automated higher order theorem provers.
The project distinguishes between three important aspects of THF0:

Syntax

The syntax of THF0 is defined as a conservative extension of the existing TPTP language formats FOF and CNF for first order logic. An advantage of this approach is that existing TPTP technology can be easily reused or adapted to also support the new THFO language. A disadvantage, however, is that the BNF for THF0 appears overly complicated and even messy. For this note that Church simple type theory has a simple, single inductive structure at term/formula level while first order logic has a more complicated, double inductive structure which explicitly distinguishes between the term level and the formula level. Church's simple type theory instead only defines typed terms and all terms of a certain type (type Boolean) are making up the formulas.

Type checking

The TPTP infrastructure does not provide type checking support for THF0. As a consequence, the THF0 syntax definition allows many meaningless terms, for example, ~ = &. Additional type checking is therefore needed to distinguish between well-typed, meaningful THF0 expressions and ill-typed, meaningless THF0 expressions. Such a type checking support for THF0 is provided via Twelf. Meaningful THF0 expressions are thus identified with the help of both the TPTP THF0 parser and the Twelf type checker for THF0.

Syntax and type checking of THF0 is thus settled and more details can be found in [1].

Semantics

An open issue in the development of the TPTP THF0 language is concerned with its semantics. The problem is that there is no obvious, canonical notion of semantics that we want to pick and stipulate for THF0. In order to illustrate the problems we briefly discuss some candidates: The above discussion shows that there are good reasons for not fixing one ultimate target semantics for THF0 in the first place. Instead, our proposal is to annotate the THF0 problem files with semantical information. For this we want to introduce an ontology of interesting notions of semantics for THF0 and let the user annotate the problem files with the most suitable target semantics for his/her application. Similarly, the provers shall provide information to which target semantics they are applicable, that is, for which target semantics they are performing sound proof search. At the TPTP party this proposal shall be sketched and further discussed.

References