Beth Cədvəlləri
Proqramınız verilmiş məntiqi formulanın düzgünlüyünü yoxlamalıdır. Əgər formula E düzgün deyilsə (yəni dəyişənlərə boolean dəyərlərin təyin edilməsi üçün 0 qiymətini alırsa), siz həmçinin belə bir təyin etməni tapmalısınız.
Adətən belə tapşırıqlar sadəcə olaraq E formulunda olan dəyişənlərə dəyərlərin bütün mümkün təyin etmələrini işləyərək həll edilir; əgər belə k dəyişən varsa, bu 2^k belə təyin etməni nəzərdən keçirməyi tələb edir. Əlbəttə, bu, k böyük dəyərləri üçün demək olar ki, mümkün deyil. Bundan başqa, bu proses insanların adətən məntiqi formulları yoxlama (yəni sübut etmə) üsulundan çox fərqlidir.
Bu tapşırıqda sizdən məntiqi formulların düzgünlüyünü yoxlamaq üçün təbii bir üsul olan Beth tabloları əsasında bir üsul tətbiq etməniz tələb olunur. Formulların düzgünlüyünü yoxlamaq üçün bu üsul müəyyən dərəcədə insanların sübutlar və ya əks nümunələr tapma prosesini modelləşdirir, ən azından, qurulmuş Beth tablolarından adətən qısa və dəqiq bir sübut dərhal əldə edilə bilər.
Gəlin nəzərə alınan məntiqi formulların sintaksisini müəyyən edək:
Sabitlər 1 və 0;
Dəyişənlər — A ilə Z və a ilə z arasında olan hərflər;
Möhtərizələr — əgər E bir formuldursa, onda (E) başqa bir formuladır;
İnkar — ¬E hər hansı bir E formulu üçün bir formuladır;
Və — E_1 ∧ E_2 ∧ ... ∧ E_n. Qeyd edək ki, və soldan sağa doğru qiymətləndirilir: E_1 ∧ E_2 ∧ E_3 = (E_1 ∧ E_2) ∧ E_3.
Və ya — E_1 ∨ E_2 ∨ ... ∨ E_n. Eyni qeyd tətbiq olunur.
İmplyasiya — E_1⇒E_2. Əvvəlki iki əməliyyatdan fərqli olaraq sağdan sola doğru qiymətləndirilir: E_1⇒E_2⇒E_3 E_1⇒(E_2⇒E_3) deməkdir.
Ekvivalentlik — E_1 ≡ E_2 ≡ ... ≡ E_n. Bu ifadə aşağıdakı kimi hesablanır: (E_1 ≡ E_2) ∧ (E_2 ≡ E_3) ∧ ... ∧ (E_{n-1} ≡ E_n).
Əməliyyatlar ən yüksək prioritetdən ən aşağıya doğru sıralanır.
Gəlin mürəkkəb formula E-nin əsas əməliyyatını E-də sonuncu icra olunan əməliyyat kimi müəyyən edək (əlbəttə, yalnız bir sabit və ya dəyişəndən ibarət olan formulların əsas əməliyyatı yoxdur). Həmçinin, gəlin formulumuzun ekvivalentlik əməliyyatları içermədiyini fərz edək, çünki biz həmişə E_1 ≡ E_2 ifadəsini (E_1⇒E_2) ∧ (E_2⇒E_1) ilə əvəz edə bilərik.
İndi Beth tablosunu iki sütunlu bir cədvəl olaraq müəyyən edək, burada bəzi formullar yazılmışdır. Sütunlarda yazılan formulların sırası və bir formulanın bir sütunda neçə dəfə göründüyü əhəmiyyətsizdir: məsələn, bütün formulların bir sütunda fərqli olduğunu və leksikoqrafik olaraq sıralandığını fərz edə bilərik.
Qeyri-rəsmi olaraq sol sütun doğru olmasını istədiyimiz formullara, sağ sütun isə yanlış olmasını istədiyimiz formullara uyğun gəlir; bütün proses sonra verilmiş E formuluna əks nümunə yaratmağa cəhd kimi qəbul edilə bilər. Bir Beth tablosu ziddiyyətli adlanır, əgər bu tabloda hər hansı bir E* formulu hər iki sütunda görünürsə, ya da sol sütunda 0 görünürsə, ya da sağ sütunda 1 görünürsə.
Prosesin hər addımında bir neçə Beth tabloları kolleksiyamız var. Biz boş sol sütun və sağ sütunda yalnız verilmiş E formulu olan bir Beth tablosu ilə başlayırıq. Prosesin bir addımı ziddiyyətli olmayan Beth tablolarından birindən mürəkkəb bir formula C seçmək və C-nin əsas əməliyyatı və C-nin yerləşdiyi sütun (sol və ya sağ) tərəfindən seçilən bir qayda tətbiq etməkdən ibarətdir. Nəticədə bu Beth tablosunun sol və ya sağ sütunlarına (və ya hər ikisinə) bəzi formullar əlavə olunur; əlbəttə, əgər əlavə etmək istədiyimiz bu formullar artıq oradadırsa, Beth tablosu dəyişməyəcək, buna görə də bu halda müvafiq qayda tətbiq edilə bilməz deyirik. Həmçinin, bəzi qaydalar orijinal Beth tablosunun iki nüsxəsini yaradır və bu nüsxələrdən birinə bəzi formullar, digərinə isə başqa formullar əlavə edir. Bu halda, əgər tətbiq olunan qayda nəticəsində əldə edilən hər iki Beth tablosu artıq kolleksiyada varsa, qayda tətbiq edilə bilməz deyirik.
Proses heç bir qayda tətbiq edilə bilmədikdə dayanır. Qeyd edək ki, qurulmuş bütün Beth tablolarında meydana gələn bütün formullar orijinal formulun alt-formulları olacaq, beləliklə yalnız sonlu sayda Beth tabloları əldə edilə bilər və beləliklə yalnız sonlu sayda Beth tabloları kolleksiyaları əldə edilə bilər. Buna görə də proses bir nöqtədə dayanmalıdır. Əgər bu nöqtədə kolleksiyadakı bütün Beth tabloları ziddiyyətlidirsə, orijinal formula E düzgün olduğu sübut edilmişdir. Əks halda, əgər τ kolleksiyadan ziddiyyətli olmayan bir Beth tablosudursa, E-də meydana gələn hər hansı bir dəyişən x τ-nin yalnız bir sütununda meydana gəlməlidir (çünki τ ziddiyyətli deyil; ən azı bir sütunda meydana gəlməlidir, çünki əks halda τ-də x olan ən qısa formul üçün bir qayda tətbiq edilə bilərdi). Sonra gəlin τ-nin sol sütunundakı bütün dəyişənlərə 1 və sağ sütunundakı dəyişənlərə 0 təyin edək. Bu, E üçün əks nümunə verəcək, yəni orijinal formulamız E üçün dəyişənlərə dəyərlərin təyin edilməsi üçün 0 qiymətini alır.
İndi bütün mümkün qaydaları sadalayaq. Artıq izah edilmişdir ki, bir qayda bir formulun C əsas əməliyyatı * və C-nin tapıldığı sütun (sol və ya sağ) ilə müəyyən edilir. Bu qaydaları * və * ilə etiketləyəcəyik, burada * əməliyyatdır (bunlardan biri ∧, ∨, ⇒ və ya ¬). Əgər * ikili əməliyyatdırsa, C = A * B fərz edəcəyik; əks halda C = ¬A fərz edirik.
Gəlin tabloların sayını artırmayan qaydaları sadalayaq (yəni onlar sadəcə olaraq seçilmiş Beth tablosunun sütunlarına bəzi formullar əlavə edirlər):
Bu aşağıdakı mənanı verir: məsələn, əgər bir Beth tablosunun sağ sütunundakı A⇒B formuluna ⇒ qaydasını tətbiq ediriksə, onda bu tablonun sol sütununa A və sağ sütununa B əlavə etməliyik.
Növbəti qaydalar bir Beth tablosundan iki Beth tablosu yaradır. Oxşar notasiya istifadə olunur, lakin hər qayda üçün iki Beth tablosu göstərilir:
Bu üç qayda aşağıdakı kimi şərh edilir: məsələn, əgər bir Beth tablosunun sol sütunundakı A ∨ B formuluna ∨ tətbiq ediriksə, τ Beth tablosunu τ' və τ" nüsxələri ilə əvəz etməliyik və sonra τ'-nin sol sütununa A və τ"-nin sol sütununa B əlavə etməliyik.
Giriş verilənləri
Girişin yeganə sətri '0', '1', 'A' ... 'Z', 'a' ... 'z', '(', ')', ' ', '', '|', '=>', '=' simvollarından ibarət bir sətir kimi təqdim olunan formulu ehtiva edir. Son beş simvol müvafiq olaraq ¬, ∧, ∨, ⇒ və ≡ üçün dayanır. Simvollar istənilən sayda boşluqla ayrılmış ola bilər. Sətir ən çox 1000 simvol ehtiva edəcək. Girişdəki formula sintaktik olaraq düzgün olacaq.
Çıxış verilənləri
Çıxışda dəqiq bir sətir olmalıdır. Əgər formula düzgündürsə, sadəcə "true" çıxış edin, əks halda "false" və formulu etibarsız edən dəyişənlərin təyin edilməsini çıxış edin. Dəyişənləri leksikoqrafik sırada sadalayın. Nümunə çıxışa mümkün qədər dəqiq riayət edin.