E 2.3 is a theorem prover for many-sorted first-order logic with equality. We describe the
basic logical and software architecture of the system, as well as core features of the …

This paper describes the TPTP problem library and associated infrastructure, from its use of
Clause Normal Form (CNF), via the First-Order Form (FOF) and Typed First-order Form …

E is a theorem prover for full first-order logic with equality. It reduces first-order problems to
clause normal form and employs a saturation algorithm based on the equational …

The considerable mathematical knowledge encoded by the Flyspeck project is combined
with external automated theorem provers (ATPs) and machine-learning premise selection …

The TPTP World is a well established infrastructure that supports research, development,
and deployment of Automated Theorem Proving (ATP) systems. There are key components …

Abstract The Thousands of Problems for Theorem Provers (TPTP) World is a well-
established infrastructure that supports research, development and deployment of …

Leo-III is an automated theorem prover for extensional type theory with Henkin semantics
and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based …

A key driver of SMT over the past decade has been an interchange format, SMT-LIB, and a
growing set of benchmarks sharing this common format. SMT-LIB captures very well an …

We introduce refutationally complete superposition calculi for intentional and extensional
clausal λ-free higher-order logic, two formalisms that allow partial application and applied …

The TPTP World is a well-established infrastructure for automatic theorem provers. It defines
several concrete syntaxes, notably an untyped first-order form (FOF) and a typed first-order …