Inductive and Deductive AI over Large Formal Libraries

Josef Urban, Radboud University Nijmegen

Overview

Henri Poincare

Poincare's opposition to set theory

Enters the Real Hero

Alan Turing 1936 - Undecidability

Alan Turing 1950 - Artificial Intelligence

Which intellectual fields to use for building AI?

Turing vs. the 1936-style CS theoreticians

Hence my depressive slide from 2011 AMS

Data driven AI (Turing 50 years later)

John Shawe-Taylor and Nello Cristiani -- Kernel Methods for Pattern Analysis (2004):

The Data driven approach

Large-theory AI/ATP agenda since 2003

How much can we AI/ATP-prove today?

High-level ATP guidance: Premise Selection

Example: Mizar Proof Advisor (2003)

Evaluation of methods on MPTP2078

ML evaluation (premise recall) ML evaluation: Recall

Evaluation of methods on MPTP2078

ATP evaluation (problems solved) ATP evaluation: Solved

Combined (ensemble) methods

Combining with SInE improves the best method from 726 to 797 (10%)