Where, What, and How? Lessons from the Evolution of E.

Artificial intelligence methods are becoming more important for premise selection in large-theory automated reasoning. The most significant application is relevance filtering, which proceeds by extracting features from premises and applying machine learning algorithms to choose the most relevant ones. Most research so far has focused improving the machine learning algorithms. Here, we investigate different mechanisms of feature extraction from premises, that do not focus on the syntactic structure of the terms, but instead on their logical semantics, taking into account matching, unification and anti-unification. We will describe an implementation of semantic features for first-order logic terms and our initial experiments with the impact of such features on the performance of automated reasoning.

Random forests are a machine learning method which has been shown to yield very good prediction speed and quality even for huge datasets: This is achieved by growing a set of decision trees randomly, which can then later be queried very efficiently. We show how to apply this method to automatic theorem proving and present our own version of online random forests.

Some Ideas about Making ATPs for Large Theories

Although Isabelle/HOL is essentially based on standard higher-order logic, it does have some technically exotic (yet very useful and heavily used) features ­- notably, a flexible mechanism for overloaded definitions, which is used in conjunction with the axiomatic type classes to achieve Haskell-like type classes in the user space. I want to briefly introduce these features in my talk and discuss the consequences of them. Among others, what is the impact on the model theory of Isabelle/HOL and how theses features complicate translation of Isabelle/HOL into other systems.

Joint Work with Dmitriy Traytel. Proof assistants are popular in some communities, e.g. programming language research and also term rewriting. Paradoxically, the automated reasoning community has been little enclined to formalize their results. We believe that proof assistants could advantageously replace paper proofs, once we have developed suitable libraries and methodology. In previous work, we (together with Andrei Popescu) formalized first-order logic with binders and sorts, skolemization, and sort encodings (FroCoS 2013, IJCAR 2014). Now we are going further by formalizing the key results from Bachmair and Ganzinger's "Resolution Theorem Proving" survey in the "Handbook of Automated Reasoning" (Vol. 1, Chap. 2, 2001) in Isabelle/HOL. We have already formalized the ground unrestricted and ordered-with-selection resolution calculus (Section 3) as well as the general saturation framework with redundancy (Sections 4.1 and 4.2) and are now lifting the results to the non-ground case (Section 4.3). In the process, we have uncovered a number of issues with the framework and the proof (but no flaws in the calculi). As future work, we would like to study superposition and variants.

We present here the export of libraries from two interactive theorem provers HOL Light and HOL4. In particular, we describe the challenges encountered when recording types, constants, theorems and their dependencies. The exported data is then parsed and organized for a future exploitation by a machine learning tool for theorem proving such as HOL(y)Hammer.

Some Algorithms for Translating between Informal and Formal Mathematics.

Multiagent planning is a coordination technique used for deliberative acting of a team of agents. One of vital planning techniques uses declarative description of agents’ plans based on Finite State Machines and their later coordination by intersection of such machines with successive verification of the resulting joint plans. In this work, we firstly propose to use projections of agents’ actions directly for multiagent planning based on iterative building of a coordinated multiagent plan. Secondly, we describe integration of the static analysis provided by process calculi type systems for approximate verification of exchanged local plans. Finally, we compare our approach with current state-of-the-art planner on an extensive benchmark set.