ABSTRACT. We discuss the topic of unsatisfiability proofs in SMT, particularly with reference to quantifier free non-linear real arithmetic. We outline how the methods here do not admit trivial proofs and how past formalisation attempts are not sufficient. We note that the new breed of local search based algorithms for this domain may offer an easier path forward.

ABSTRACT. We present a way to analyze the complexity of theorem proving strategies in an implementation independent manner.

ABSTRACT. Evaluating automatic theorem provers is a non-trivial, subtle endeavour. There are a number of conflicting issues to consider, be they computational, statistical, economic, or — most difficult of all — social. We present a review of such challenges, seen from the perspective of, and with application to, the first-order system Vampire. We further highlight the exemplary achievements of existing thought and practical tools, and sketch some future directions for work in this area. We are not the first to consider this issue and do not claim to offer the final word but believe strongly that this is a topic that requires significant and sustained attention from our community.

ABSTRACT. In the past abstractions have been used as a guide to the structure of a proof. Here we propose to use them instead as a means to select relevant clauses from a large set of clauses.

ABSTRACT. The Thousands of Problems for Theorem Provers (TPTP) World is a rich infrastructure that supports the development, deployment, and application of Automated Theorem Proving (ATP) for classical logics. This paper describes proposed expansion and modernisation of some parts of the TPTP World: the TPTP Problem library, a new TDTP Data library, new logics and languages, and improved user services. Hopefully this will attract suggestions, feedback, and offers of support to help achieve these goals.

ABSTRACT. There is a need for help in the long term management of the TPTP problem set. We propose to discuss various possibilities for this.