Talk: Training ENIGMAs, CoPs, and other thinking creatures
Abstract: The talk will mainly discuss several recent AI/TP systems and experiments that combine reasoning with learning in positive feedback loops. I will try to describe the settings, the datasets that may today contain millions of proofs, the interesting parts of the algorithms, and some of the practical challenges when building learning-guided systems that actually prove theorems in real time. Time permitting, I will also discuss the outlook, interesting future directions and initial experiments related to them.
Talk: The Logic Languages of the TPTP World
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.