-
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.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
بررسی رفتار بادبندهای مرکب نسبت به رفتار بادبندهای متداول موجود در سازه های فولادی
-
کاربرد پارچه در تقویت مصالح ساختمانی
-
بررسی میزان برخورداری کتاب هدیه های آسمانی چهارم ابتدایی از مؤلفه های پدیده ی جهانی شدن
-
tripled fixed point theorems for contractive type mappings in partially ordered metric spaces
-
the communicative function of english verb number
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
ارایه الگوی تلفیقی مکان یابی ویژه گردشگری ورزشی با بکارگیری سیستم اطلاعات جغرافیایی (gis) و روش رویهم گذاری لایه ها (io)
-
تنبیه بدنی کودکان در اسناد بین المللی
-
سرمایه گذاران نهادی، سیاست تقسیم سود و ارزش شرکت
-
شناسایی عوامل موثر بر سرمایه گذاری خرد و تدوین مدل در قراردادهای آتی سکه بورس کالایی ایران
-
بررسی تاثیر عدالت از قیمت درک شده و رضایت بر وفاداری با نقش میانجی قصد مجدد خرید (مشتریان رستوران شهرزاد اصفهان)
سوال خود را در مورد این مقاله مطرح نمایید :