Sübut Generatoru#1401
Məntiqi formulun sintaksisi şəkil 1(a)-da göstərilmişdir, burada dəyişən həqiqət dəyərini ifadə edir. (\textbf{+ F_1 \ldots F_n}) formulu \textbf{F_i} formulalarının məntiqi disjunkiyası (və ya) deməkdir, (\textbf{* F_1 \ldots F_n}) formulaların məntiqi konjunksiyası (və) deməkdir, və isə formulunun inkarıdır. Əgər bir formul şəkil 1(b)-də verilmiş xüsusi sintaksisə malikdirsə, bu zaman həmin formul ACM Normal Forması (ACMNF) vəziyyətindədir deyilir.
Bir formul ACMNF-ə aşağıda verilmiş çevirmə qaydalarından istifadə etməklə çevrilir, burada formul, formulaların boş olmayan ardıcıllığı, və isə ehtimal ki, boş olan formul ardıcıllıqlarıdır. \textbf{q} \rightarrow \textbf{r} çevirmə qaydasını formul -ə tətbiq etmək deməkdir ki, formulunun quruluşuna uyğun gələn hissəsi ilə əvəzlənir, bu da şəkil 2-də göstərilmişdir. Çevirmə zamanı, heç bir çevirmə qaydası tətbiq edilə bilmədikdə proses bitir. Hər bir formul üçün çevirmə mütləq sona çatır və nəticə, qaydaların hansı ardıcıllıqla və formulun hansı hissələrinə tətbiq edilməsindən asılı olmayaraq, unikal olur.
Aksiomlar dəsti yalan dəyərlər siyahısı (\textbf{V_1} \textbf{V_2} \ldots \textbf{V_n}) kimi verilir. Aksiomlar dəstinə görə formul -in isbatı elə bir ACMNF terminidir ki, bu termin üzərində doğrudur. Məsələn, formulunun aksiomlarına görə isbatları və terminləridir.
Tapşırıq belədir: verilmiş formulu, aksiomlar dəsti və k_1, \ldots, k_n ədədləri üçün avtomatik isbat generatoru yazın ki, formulunun ACMNF-ində göründüyü qaydada növbəti isbatları çıxışa versin. Əgər isbatlar tükənsə, generator həmişə ilk isbata qayıdaraq davam edir. Məsələn, formulunun aksiomlarına görə ilk isbatı olur. Üç isbat da ard-arda generasiya edilərsə, nəticələr belə alınır: , , və . Əgər ACMNF formulunda eyni terminlər varsa, şəkil 3-dəki son nümunədə olduğu kimi, bu terminlər fərqli sayılır.
Isbat generatoru standart girişdən verilənlər toplusunu oxumalıdır. Bir verilənlər dəstinin məzmunu belədir: \textbf{F}\ \textbf{A}\ \textbf{k_1}\ \ldots\ \textbf{k_n}\ 0, burada n > 0, — formul, — aksiomlar dəsti, \textbf{k_1}, \ldots, \textbf{k_n} isə -dan fərqli uzun tam ədədlərdir. Hər \textbf{k_i} üçün (i=1, \ldots, n) proqram formulunun növbəti |\textbf{k_i}| qədər isbatını generasiya etməli və əgər \textbf{k_i} > 0-dırsa, həmin isbatları standart çıxışa çap etməlidir.
Çap olunmuş hər isbat sətirin əvvəlindən başlamalıdır, və isbat simvolları arasında heç bir boşluq olmamalıdır. Əgər \textbf{k_i} < 0-dırsa, generasiya olunmuş isbatlar çap edilməməlidir. Girişdə boşluqlardan sərbəst istifadə oluna bilər. Bir formul maksimal simvoldan ibarət ola bilər və ACMNF termini (boşluqlar nəzərə alınmadan) ən çox simvol ola bilər. Giriş verilənləri son-of-file ilə bitir və düzgündür.
Nümunə 1