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

  • reducing higher-order theorem proving to a sequence of sat problems

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 744
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     we describe a complete theorem proving procedure for higher-order logic that uses sat-solving to do much of the heavy lifting. the theoretical basis for the procedure is a complete, cut-free, ground refutation calculus that incorporates a restriction on instantiations. the refined nature of the calculus makes it conceivable that one can search in the ground calculus itself, obtaining a complete procedure without resorting to meta-variables and a higher-order lifting lemma. once one commits to searching in a ground calculus, a natural next step is to consider ground formulas as propositional literals and the rules of the calculus as propositional clauses relating the literals. with this view in mind, we describe a theorem proving procedure that primarily generates relevant formulas along with their corresponding propositional clauses. the procedure terminates when the set of propositional clauses is unsatisfiable. we prove soundness and completeness of the procedure. the procedure has been implemented in a new higher-order theorem prover, satallax, which makes use of the sat-solver minisat. we also describe the implementation and give several examples. finally, we include experimental results of satallax on the higher-order part of the tptp library.

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

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