Libraries of Formalized Mathematics - Deductive AI Meets the Inductive AI

Deductive Artificial Intelligence

• Most Advanced: Automated Theorem Proving (ATP)
• Whate else? Proof assistants, planning, deduction in ontologies, NLP application,...
• Others often use ATP as a black-box "deduction machine"

Simple brute force approaches winning

• Propositional implementations winning over first-order whenever possible
• Clausal representation winning over full first-order whenever possible
• First-order representation winning over higher-order whenever possible
• Classical first-order representation winning over various extended logics (probability, fuzzy, modal, situation, temporal, ...)

Inductive Artificial Intelligence

• Machine Learning
• Data Mining, Knowledge Discovery in Databases
• Many applications in recent years: Google, direct marketing
• Inductive reasoning: induce conjectures from large databases, verify them on test data by statistical methods

Simple brute force approaches winning

• Number of well-known propositional methods: Neural Nets, Decision Trees, Bayes Nets, Nearest-Neighbour, Hidden Markov Models
• Number of very efficient implementations and toolkits available for them
• First-order systems: Progol, FOIL, Aleph - more expressive, much less able to handle large amounts of data
• Even the succesful first-order systems use quite simple brute force algorithms

Libraries of Formalized Mathematics

• About the last 15 years - the Mizar Mathematical Library
• Primarily deductive methods
• Today large enough for inductive methods
• Inductive methods not only possible, they are necessary, the search space is too big for deductive methods only

Deduction in Libraries of Formalized Mathematics

• Mizar checker - fast but very limited, user must be wise
• Theorem proving - slower, can be very strong, problems with > 500 initial formulas hard to solve

Induction in Libraries of Formalized Mathematics

• Learn from the previous proofs given in the library
• Use the extracted experience to advise humans: Mizar Proof Advisor http://lipa.ms.mff.cuni.cz/~urban/posdemo.html
• Now Bayesian methods (the SNOW system) - many other propositional algorithms possible

Combining Deduction and Induction

• Use the extracted experience to advise theorem provers
• The MPTP systems together with the Mizar Proof Advisor
• Two brute force approaches: the inductive mathod is used to cut down the search space of the deductive method
• Is it enough, or do we need a tighter integration?