Abstract
A stable proposal for extending the first-order TPTP (Thousands of Problems for Theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. The purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. Design goals are discussed. BNF2, a new specification language, is presented. Unix/Linux scripts translate the specification document into a lex scanner andyacc parser.