In practice, today's best ATP system are however still far weaker than trained mathematicians in most research domains. Machine learning from many proofs could be used to improveonthis.

This paper describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to higher-order logic in the TPTP language using an embedding approach, and solved using higher-order logic ATP systems. Additionally, the results from native modal logic ATP systems are considered, and compared with those from the embedding approach. The findings are that the embedding process is reliable and successful, the choice of backend ATP system can significantly impact the performance of the embedding approach, native modal logic ATP systems outperform the embedding approach, and the embedding approach can cope with a wider range modal logics than the native modal systems considered.

Best papers of the workshop, after further revisions and independent reviews, will be considered for publication in a special issue of a renowned journal. By this holistic view we encounter a variety of challenges along the AI modeling cycle and software system engineering lifecycle as outlined in the figure below such as: • theory-practice gap in machine learning with impact on stability, reproducibility or integrity due to limitations of nowadays theoretical foundations in statistical learning theory or lack of control of high-dimensionality effects of deep learning; • facing computational constraints, e.g. All submissions will be peer-reviewed by, at least, 3 reviewers and judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the workshop. Short papers are meant for timely discussion and feedback at the workshop. Papers are accepted with the understanding that at least one author will register for the conference to present the paper.

You are invited to prepare an extended abstract to be considered for presentation at the 2020 Oil & Gas HPC Conference hosted by the Ken Kennedy Institute at Rice University. The conference is the premier meeting place for HPC users and participants to engage in conversations about challenges and opportunities in high performance computing, computational science and engineering, and data science across the energy industry. Attended by more than 500 leaders and experts from the energy industry, academia, national labs, and IT industry, this is a unique annual opportunity for key stakeholders to engage and network to help advance HPC in the industry. Computation, data, and information technology continue to stand out across the energy industry as critical business enablers. Recent advances in machine learning, deep learning, robotics and AI are emerging, and there is convergence between these emerging areas and HPC. With the end of Moore's law, challenges are mounting around a rapidly changing technology landscape. However, the end of one era is also an opportunity for advancements and the beginning of a new era – a renaissance for system architectures highlights the need for investments in people (workforce), algorithms, software innovations, and hardware platforms to support system scalability and demands for increasing digitization across the oil and gas sector.

We develop a vector space semantics for verb phrase ellipsis with anaphora using type-driven compositional distributional semantics based on the Lambek calculus with limited contraction (LCC) of J\"ager (2006). Distributional semantics has a lot to say about the statistical collocation-based meanings of content words, but provides little guidance on how to treat function words. Formal semantics on the other hand, has powerful mechanisms for dealing with relative pronouns, coordinators, and the like. Type-driven compositional distributional semantics brings these two models together. We review previous compositional distributional models of relative pronouns, coordination and a restricted account of ellipsis in the DisCoCat framework of Coecke et al. (2010, 2013). We show how DisCoCat cannot deal with general forms of ellipsis, which rely on copying of information, and develop a novel way of connecting typelogical grammar to distributional semantics by assigning vector interpretable lambda terms to derivations of LCC in the style of Muskens & Sadrzadeh (2016). What follows is an account of (verb phrase) ellipsis in which word meanings can be copied: the meaning of a sentence is now a program with non-linear access to individual word embeddings. We present the theoretical setting, work out examples, and demonstrate our results on a toy distributional model motivated by data.

One of the more important aims of graduate artificial intelligence courses is to prepare graduate students to critically evaluate the current literature. The established approaches for this include either asking a student to present a paper in class, or to have the entire class read and discuss a paper. However, neither of these approaches presents incentives for student participation beyond the posting of a single summary or review. In this paper, we describe a class project that uses the popular Easychair conference management system as a pedagogical tool to enable engagement in the peer review process. We report on the deployment of this project in a medium-sized graduate AI class, and present the results of this deployment. We hope that the success of this project in engaging students in the peer review process can be used better train and bolster the future corps of AI reviewers.