MoMM - Fast Interreduction and Retrieval in Large Libraries of

Motivation

• Fast retrieval of matching theorems from MML (40000 formulas)
• Interestingness : Is it possible? Can it be done easily?
• More advanced applications
• Interreduction of theorems - find redundant
• Export of internal Mizar lemmas (900000 formulas)
• Statistics about usage of theorems and lemmas
• Upgrade frequent lemmas to theorems
• Restructuring of MML, Data Mining
• Type-aware subsumption?

Implementation ideas

• Database indexing good as prefilter, hard to extend to terms
• Full theorem proving - we do not want inferences
• Indexing methods and data structures in ATPs - that's it
• E prover (Stephan Schultz) - GPL, nicely written
• Perfect discrimination trees
• CSSCPA tool (Sutcliffe, Schultz) - subsumption tool

Implementation adjustments

• Large signature of MML (7000 symbols)
• Memory: Use of splay trees instead of arrays at PDTree nodes
• Speed: Signature pretest before subsumption
• Speed: hard limit (1000) to the literal matching attempts
• Strength: Typed subsumption similar to Mizar's

Additional MoMM functionality

• Options and statuses controlling insertion and checking
• Options controlling type mechanisms (type-table loading)
• Dumping both the termbanks and the clausebanks, fast loading
• Functions in the Mizar Emacs interface

Functions in the Mizar Emacs interface

• Load all MML theorems (140 M, 14s on P4 3GHz)
• Load theorems depending on article's environment
• Load generalized internal lemmas
• Export currently written article and load it too
• Ask MoMM for help interactively

Interreduction results

• 65702 clauses created from theorems and definitions
• Full interreduction: 9 minutes on P4 3GHz
• 1695 of them redundant - not always removable from the MML
• Interreduction of the 860000 internal lemmas: 36 minutes
• More than half of them subsumed
• Most of Mizar Matches!

Typed Subsumption in MoMM

• Mizar: Term-dependant types:
• Filter of X -> Subset-Family of X
• Mizar attributes: X is non empty finite set
• Mizar clusters: empty -> finite set
• Make the subsumption aware of the type hierarchy
• Can be done as a simple type-table in MoMM
• Make the subsumption aware of the cluster theories
• More difficult
• Subsumption must match the types of new bindings

Conclusion, Future Work

• It can be done with normal hardware
• The ATP technology quite suitable for Mizar
• Large libraries need more automated control
• Real-time accessible central repository of math?
• Limited theorem proving?
• Second order features?

-- JosefUrban - 07 Jul 2004