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

  • extending sledgehammer with smt solvers

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 689
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     sledgehammer is a component of isabelle/hol that employs resolution-based first-order automatic theorem provers (atps) to discharge goals arising in interactive proofs. it heuristically selects relevant facts and, if an atp is successful, produces a snippet that replays the proof in isabelle. we extended sledgehammer to invoke satisfiability modulo theories (smt) solvers as well, exploiting its relevance filter and parallel architecture. the atps and smt solvers nicely complement each other, and isabelle users are now pleasantly surprised by smt proofs for problems beyond the atps’ reach.

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

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