zbMATH — the first resource for mathematics

The TPTP typed first-order form with arithmetic. (English) Zbl 1352.68217
Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 406-419 (2012).
Summary: The TPTP World is a well established infrastructure supporting research, development, and deployment of Automated Theorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. This paper describes these developments.
For the entire collection see [Zbl 1238.68012].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI