محبوبترین نویسندگان :
نویسندگان مقالات پربازدید :
مجله استدلال خودکار 2013
جزئیات رویداد
همایش ، رویداد ، ژورنال
اینستاگرام تی پی بین

  • conjecture synthesis for inductive theories

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 812
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     we have developed a program for inductive theory formation, called isacosy, which synthesises conjectures ‘bottom-up’ from the available constants and free variables. the synthesis process is made tractable by only generating irreducible terms, which are then filtered through counter-example checking and passed to the automatic inductive prover isaplanner. the main technical contribution is the presentation of a constraint mechanism for synthesis. as theorems are discovered, this generates additional constraints on the synthesis process. we evaluate isacosy as a tool for automatically generating the background theories one would expect in a mature proof assistant, such as the isabelle system. the results show that isacosy produces most, and sometimes all, of the theorems in the isabelle libraries. the number of additional un-interesting theorems are small enough to be easily pruned by hand.

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

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