حذف عطف
ظاهر
گونه | قاعده استنتاج |
---|---|
گرایش | حساب گزارهای |
گزاره | اگر ترکیب عطفی و درست باشد، آنگاه هر دوی و درست هستند. |
بیان نمادین |
|
قاعده استنتاج |
---|
حساب گزارهای |
قاعده استنتاج |
Rules of replacement |
منطق مرتبه اول |
در حساب گزارهای، حذف عطف (به انگلیسی: Conjunction elimination)[۱] یک استدلال مباشر معتبر، صورت منطقی و قاعدهٔ استنتاج است که این استنتاج را میسازد که اگر ترکیب عطفی و درست باشد، آنگاه هر دوی و درست هستند.
این قاعده شامل دو قاعدهٔ فرعی جداگانه است که میتواند به زبان صوری بهصورت زیر بیان شود:
و
دو قاعدهٔ فرعی با هم به این معنی است که هر زمان که یک نمونه از ""در خط یک اثبات ظاهر میشود، "" یا "" را میتوان به تنهایی در خط بعدی قرار داد.
نشانهگذاری بهشکل صوری
[ویرایش]قواعد فرعی حذف عطف ممکن است بهصورت زیر نوشته شوند:
و
و همچنین یک نماد فرامنطق است که به این معنی است که نتیجهٔ منطقی و است و همچنین یک نتیجهٔ نحوی از در دستگاه صوری میباشد.
و میتوانند بهصورت همانگوییهای حساب گزارهای بیان شوند:
و
منابع
[ویرایش]- ↑ David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley. Sect.3.1.2.1, p.46