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

  • a two-level logic approach to reasoning about computations

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 883
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. we therefore propose a (restricted) logical theory over relations as a language for specifying such notions. our specification logic is further characterized by an ability to explicitly treat binding in object languages. once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. we propose to use a second logic, called a reasoning logic, for this purpose. a satisfactory reasoning logic should be able to completely encode the specification logic. associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. to provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. we provide these capabilities here by using a logic called g which represents relations over λ-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. we show how provability in the specification logic can be transparently encoded in g. we also describe an interactive theorem prover called abella that implements g and this two-level logic approach and we present several examples that demonstrate the efficacy of abella in reasoning about computations.

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

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