Many-valued Logic in HOL

دسته بندی: منطق
ویرایش:  
نویسندگان: Polak Indra.  
سری:  
 
ناشر:  
سال نشر:  
تعداد صفحات: 15 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 250 کیلوبایت 

قیمت کتاب (تومان) : 55,000

اینترنت-انتشارات. - 15 ص. (ص: 113-127). انگلیسی. Abstract.
منطق چند ارزشی در منطق قضیه اثبات کننده HOL [GM93] رسمیت یافته است. ما یک رویکرد جبری را دنبال می کنیم، که از جبر Heyting شروع می شود. با استفاده از این رویکرد و برخی ماشین آلات مفید HOL، ما یک بررسی کننده توتولوژی برای یک منطق گزاره ای سه ارزشی اجرا کردیم. مقدمه.
در حال حاضر، یک زبان مشخصات جدید در دپارتمان علوم محاسباتی در گرونینگن در دست ساخت است که زبان مشخصات تقریبا رسمی، AFSL [Saa] نام دارد. معناشناسی AFSL مبتنی بر منطق سه ارزشی است. 1 ما می خواهیم به کاربران AFSL یک \"محیط مشخصات\" مناسب، مشابه یک \"محیط برنامه نویسی\" ارائه دهیم. از آنجایی که منطق نقش مهمی در AFSL بازی می کند، یک اثبات کننده قضیه ممکن است رسانه مناسبی برای آزمایش اشکال مختلف پشتیبانی ابزار برای زبان باشد. یک اثبات قضیه برای کمک به فرآیند اثبات معتبر است. بنابراین، هر اثبات کننده قضیه دارای یک نظام اثباتی یا منطقی است که در آن قضایا اثبات می شوند. این به این معنی است که تمام اثبات هایی که می خواهیم با اثبات... مقدمه.
HOL.
نقطه شروع: جبر هیتینگ.
تاکتیک برای پشتیبانی اثباتی.
بازنویسی.
تاکتیک های هوشمند.
استقرا.
نظرات کلی.
مثال: بررسی توتولوژی برای سه منطق گزاره‌ای ارزشمند.
تاکتیک.
نتیجه‌گیری و آینده کار.
تشکرات.
ضمیمه:
- تاکتیک‌ها.
- تاکتیک‌ها.
- مولدهای قضیه.
- توابع ML.
مرجع.

Internet-Publication. — 15 p. (pp.: 113-127). English. Abstract.
Many-valued logic is formalized in the logic of the theorem prover HOL [GM93]. We follow an algebraic approach, starting from a Heyting algebra. Using this approach and some useful HOL machinery, we implemented a tautology-checker for a three-valued propositional logic. Introduction.
Currently, a new specification language is under construction at the department of Computing Science in Groningen, called Almost Formal Specification Language, AFSL [Saa]. The semantics of AFSL is based on a three-valued logic. 1 We want to provide users of AFSL with a proper 'specification environment', analogous to a 'programming environment'. Since logic plays an important role in AFSL, a theorem prover might be the right medium to test different forms of toolsupport for the language. A theorem prover is to assist the process of making valid proofs. Therefore, each theorem prover has a proof system or logic in which the theorems are proven. This implies that all proofs we want to make with the prove... Introduction.
HOL.
Starting Point: a Heyting Algebra.
Tactics for Proof Support.
Rewriting.
Smart Tactics.
Induction.
General comments.
Example: A Tautology Checker for Three Valued Propositional Logic.
The Tactic.
Conclusions and Future Work.
Acknowledgements.
Appendix:
- Tacticals.
- Tactics.
- Theorem generators.
- ML-functions.
References.