صورت بهنجار فصلی

در منطق بولی، یک صورت بهنجار فصلی یا فرم نرمال فصلی DNF یک استاندارد ( یا نرمال شده ) از یک فرمول منطقی است که یک جداکننده عبارات عطفی است. از سوی دیگر به صورت and وor هایی است که ان را به عنوان حاصل ضرب مجموع می شناسید. همچنین یک صورت بهنجار برای اثبات خودکار قضایا مفید است. یک فرمول منطقی در فرم دی اِن اف در نظر گرفته شده است اگر و تنها اگر به صورت یک فصل یاچند اتصال از یک یا چند عملگر باشد. اگر هر یک از متغیرهای دی اِن اف دقیقاً یک بار در هر عبارت باشند، فرمول دی اِن اف به طور کامل درصورت بهنجار فصلی است. مانند صورت بهنجار سی اِن اف، تنها عملگرهای گزاره ای در نات , and , or , دی اِن اف هستند. عملگر نات تنها می تواند به عنوان بخشی از عملگر استفاده شود به این معنی که فقط می تواند قبل از یک متغیر گزاره ای بیاید. برای مثال همه فرمول های زیر در فرم دی اِن اف است:
A ∧ B
A
( A ∧ B ) ∨ C
( A ∧ ¬ B ∧ ¬ C ) ∨ ( ¬ D ∧ E ∧ F )
بنابراین فرمول های زیر در فرم دی اِن اف نیستند
¬ ( A ∨ B ) — نات بیرونی ترین عملگر است
A ∨ ( B ∧ ( C ∨ D ) ) — اُر درون اَند قرار گرفته است
تبدیل یک فرمول به دی اِن اف شامل استفاده از معادله های منطقی مانند حذف دو منفی، قوانین دمورگان و قانون توزیع است. تمام فرمول های منطقی را می توان به شکل نرمال فصلی تبدیل کرد. با این حال در برخی موارد تبدیل به دی اِن اف می تواند به انفجار نمایی از فرمول منجر شود. به عنوان مثال فرمول منطقی زیر ۲ به توان n جمله دارد
( X 1 ∨ Y 1 ) ∧ ( X 2 ∨ Y 2 ) ∧ ⋯ ∧ ( X n ∨ Y n )
هر تابع بولی خاص را می توان بایک و تنها یک صورت بهنجار کامل فصلی، یکی از دوشکل متعارف، نشان داد. در زیر یک گرامر از صورت بهنجار دی اِن اف وجود دارد
• disjunct → conjunct
• disjunct → disjunct ∨ conjunct
• conjunct → literal
• ( conjunct → ( conjunct ∧ literall
• literal → variable
• literal → ¬variable
که در ان یک متغیر هر متغیری می تواند باشد
فرم های نرمال اصلی
در بعضی از سوالات از ما انتظار می رود که بتوانیم یک عبارت شرطی را برحسب پی دی اِن اف یا پی سی اِن اف بنویسیم که چندین راه برای این کار وجود دارد ولی اسان ترین راه کشیدن جدول به طریق زیر است: