ABSTRACT. The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. This talk provides an overview of the logic languages of the TPTP World, from classical first-order form, through typed first-order form, up to typed higher-order form, and beyond to non-classical forms. The logic languages are described in a non-technical way, and are illustrated with examples using the TPTP language. The second part of the talk describes the current (underdeveloped?) representation and use of proofs and models in the TPTPWorld. Topics covered include the SZS ontology; the representation of derivations and finite models; the TSTP solution library; tools for examining and manipulating the derivations; uses of individual solutions, and the TSTP as a whole; projects that have used the TPTP format and tools for proofs and models; the proposed "Tons of Data for Theorem Provers" library; future work and directions to improve the status quo.

ABSTRACT. Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence, computer science, mathematics, and philosophy. The de-facto standard infrastructure for automated theorem proving, the TPTP World, currently supports only classical logics. This paper describes the latest extension of the TPTP World, providing languages and infrastructure for reasoning in non-classical logics. The extension integrates seamlessly with the existing TPTP World.

ABSTRACT. Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinator term these straightforwardly factor into shared subgraphs. To search for proofs, combinator terms can be enumerated, like clausal tableaux, with simultaneously relating formulas associated with components of the enumerated structures through unification. To restrict the search space, the enumeration can be based on proof schemas defined as parameterized combinator terms. We introduce here this "combinator term as proof structure" approach to automated first-order proving, present an implementation and first experimental results. The approach builds on a term view of proof structures rooted in condensed detachment and the connection method. It realizes features known from the connection structure calculus, which has not been implemented so far.

ABSTRACT. The logic embedding tool encodes non-classical reasoning problems into classical higher-order logic. It is easily extensible and can support an increasing number of different non-classical logics as reasoning targets. When used as pre-processor or library for higher-order theorem provers, the tool admits off-the-shelf automation for logics for which otherwise few to none provers are available.

ABSTRACT. Choosing hardware for theorem proving is no simple task: automated provers are highly complex and optimized programs, often utilizing a parallel computation model, and there is little prior research on the hardware impact on prover performance. To alleviate the problem for Isabelle, we initiated a community benchmark where the build time of HOL-Analysis is measured. On 54 distinct CPUs, a total of 669 runs with different Isabelle configurations were reported by Isabelle users. Results range from 107s to over 11h. We found that current consumer CPUs performed best, with an optimal number of 8 to 16 threads, largely independent of heap memory. As for hardware parameters, CPU base clock affected multi-threaded execution most with a linear correlation of 0.37, whereas boost frequency was the most influential parameter for single-threaded runs (correlation coefficient 0.55); cache size played no significant role. When comparing our benchmark scores with popular high-performance computing benchmarks, we found a strong linear relationship with Dolfyn (R² = 0.79) in the single-threaded scenario. Using data from the 3DMark CPU Profile consumer benchmark, we created a linear model for optimal (multi-threaded) Isabelle performance. When validating, the model has an average R²-score of 0.87; the mean absolute error in the final model corresponds to a wall-clock time of 46.6s. With a dataset of true median values for the 3DMark, the error improves to 37.1s.