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

  • contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 913
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     in this paper we present lsj, a contraction-free sequent calculus for intuitionistic propositional logic whose proofs are linearly bounded in the length of the formula to be proved and satisfy the subformula property. we also introduce a sequent calculus rj for intuitionistic unprovability with the same properties of lsj. we show that from a refutation of rj of a sequent σ we can extract a kripke counter-model for σ. finally, we provide a procedure that given a sequent σ returns either a proof of σ in lsj or a refutation in rj such that the extracted counter-model is of minimal depth.

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

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