Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation

Abstract. A stable proposal for extending the rst-order TPTP (Thou-sands of Problems for Theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. The pur-pose 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 specication language, is presented. Unix/Linux scripts translate the specication document into a lex scanner and yacc parser.