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

  • a tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 859
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     in this paper we provide the first (as far as we know) direct calculus deciding satisfiability of formulae in negation normal form in the fragment of fhl (full hybrid logic with the binder, including the global and converse modalities), where no occurrence of a universal operator is in the scope of a binder. by means of a satisfiability preserving translation of formulae, the calculus can be turned into a satisfiability decision procedure for the fragment \textsffhl∖□↓□, i.e. formulae in negation normal form where no occurrence of the binder is both in the scope of and contains in its scope a universal operator. the calculus is based on tableaux and termination is achieved by means of a form of anywhere blocking with indirect blocking. direct blocking is a relation between nodes in a tableau branch, holding whenever the respective labels (formulae) are equal up to (a proper form of) nominal renaming. indirect blocking is based on a partial order on the nodes of a tableau branch, which arranges them into a tree-like structure.

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

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