My Position on the TPTP

Introduction

My interest is in using TPTP for reasoning on large theories, in which many axioms are irrelevant for any given query. This conforms to a typical situation in expert systems or decision support where a comprehensive knowledge base is loaded and questions need to be answered in real time.

Arithmetic

A wide variety of practical reasoning problems require arithmetic. While computation on ground formulas is often needed, just as important is simple equation solving such as 2+X=Y where X is found through some inference or lookup and Y is then computed either as a final or intermediate result.

Higher Order

Many practical reasoning problems require higher order reasoning, or at least what appears to be higher order. A simple extension that's still first order would be to allow unification on lists, rather than having to treat embedded formulas as constants.

Other Issues

While not strictly the domain of the TPTP language itself, I'm most interested in reasoners that have a few basic abilities to:

have multiple queries or assertions without reloading an entire knowledge base (or at least have an exceptionally fast load time for very large theories)
report full proofs for answers
provide bindings for variables in a query, not just state that the query can be satisfied
ask for one or many bindings for a query variable (ex. show me five UN general secretaries)
support query time limits

Conclusion

I believe that these issue present interesting scientific challenges and also potentially increase the relevance and utility of TPTP and provers that support it for a wider community of users.