• classical logic with partial functions

    نویسندگان :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 767
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     we introduce a semantics for classical logic with partial functions, in which ill-typed formulas are guaranteed to have no truth value, so that they cannot be used in any form of reasoning. the semantics makes it possible to mix reasoning about types and preconditions with reasoning about other properties. this makes it possible to deal with partial functions with preconditions of unlimited complexity. we show that, in spite of its increased complexity, the semantics is still a natural generalization of first-order logic with simple types. if one does not use the increased expressivity, the type system is not stronger than classical logic with simple types. we will define two sequent calculi for our semantics, and prove that they are sound and complete. the first calculus follows the semantics closely, and hence its completeness proof is fairly straightforward. the second calculus is further away from the semantics, but more suitable for practical use because it has better proof theoretic properties. its completeness can be shown by proving that proofs from the first calculus can be translated.

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

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