• premise selection for mathematics by corpus analysis and kernel methods

    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 1330
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. this work develops learning-based premise selection in two ways. first, a fine-grained dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for atp-based re-verification and for training premise selection algorithms. second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. to evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed, extending the older mptp challenge benchmark. the combined effect of the techniques results in a 50 % improvement on the benchmark over the state-of-the-art vampire/sine system for automated reasoning in large theories.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین ژورنال ها