چارچوب منطقی

یک چارچوب منطقی (به انگلیسی: Logical framework)، در علم منطق، راهی برای تعریف (یا نمایش) یک منطق به صورت یک امضا در نظریه نوع سطح بالاتر فراهم می‌بیند، این کار به شیوه‌ای انجام می‌شود که اثبات‌پذیری یک فرمول در منطق اصلی به مسئله اسکان نوع در نظریه نوع چارچوب کاهش می‌یابد.^[۱]^[۲] این دیدگاه برای اثبات قضیه خودکار (تعاملی) به صورت موفق استفاده شده‌است. اولین چارچوب منطقی اوتومَث (Authomath) بود؛ با این حال، نام این ایده از چارچوب منطقی ادینبورگ (LF) گرفته شده‌است که مشهورتر می‌باشد. ابزارهای اثبات جدیدتر مثل ایزابلی (Isabelle) بر اساس این ایده می‌باشند.^[۱] برخلاف جاسازی مستقیم، دیدگاه چارچوب منطقی امکان آن را فراهم می‌سازد تا تعداد زیادی منطق، در یک سیستم نوع مشابه جاسازی شوند.^[۳]

پانویس

↑ ^۱٫۰ ^۱٫۱ Bart Jacobs (2001). Categorical Logic and Type Theory. Elsevier. p. 598. ISBN 978-0-444-50853-9.
↑ Dov M. Gabbay, ed. (1994). What is a logical system?. Clarendon Press. p. 382. ISBN 978-0-19-853859-2.
↑ Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Language Engineering and Rigourous (sic) Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers. Springer. p. 48. ISBN 978-3-642-03152-6.

منابع

مشارکت‌کنندگان ویکی‌پدیا. «Logical framework». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۱۷ ژوئن ۲۰۲۰.

این یک مقالهٔ خرد منطق است. می‌توانید با گسترش آن به ویکی‌پدیا کمک کنید.

[Jacobs2001-1] ۱٫۰ ^۱٫۱ Bart Jacobs (2001). Categorical Logic and Type Theory. Elsevier. p. 598. ISBN 978-0-444-50853-9.

[Gabbay1994-2] Dov M. Gabbay, ed. (1994). What is a logical system?. Clarendon Press. p. 382. ISBN 978-0-19-853859-2.

[BoveBarbosa2009-3] Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Language Engineering and Rigourous (sic) Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers. Springer. p. 48. ISBN 978-3-642-03152-6.

[۱]

[۲]

[۳]