Conclusion

Theorem Proving in the Large

• Black box ATP systems are tools
• Complex systems (including people) are users
• Real world problems are rich and hard
• Build higher level systems for ATP deployment

Current and Future Work

• Improved relevance measures
• Use of automaticaly generated lemmas
• Component integration, evaluation, tuning
• Application to ontologies