Sübut Generatoru
Məntiqi formula, 1(a) şəklində göstərilən sintaksisə malikdir, burada dəyişən həqiqət dəyərini ifadə edir. (+ F_1 ... F_n) formulu F_i formullarının məntiqi disjunktsiyasını, (* F_1 ... F_n) formulu isə F_i formullarının məntiqi konjunktsiyasını ifadə edir. F formulu isə F-in inkarını göstərir. Əgər bir formula 1(b) şəklində verilmiş xüsusi sintaksisə malikdirsə, biz deyirik ki, formula ACM Normal Formada (ACMNF) yerləşir.
Formula aşağıda verilmiş yenidən yazma qaydaları ilə ACMNF-ə çevrilir. Burada F bir formulu, S formulların boş olmayan ardıcıllığını, s və s' isə ehtimal ki, boş olan formulların ardıcıllığını ifadə edir. Bir formulanın q→r qaydasına uyğun olaraq yenidən yazılması, F formulanın q şablonuna uyğun gələn hissəsini r ilə əvəz etmək deməkdir, 2-ci şəkildə göstərildiyi kimi. Çevrilmə, heç bir yenidən yazma qaydası tətbiq edilə bilmədikdə sona çatır. Çevrilmə hər hansı bir formula üçün sona çatır və nəticə unikaldır, hansı qaydaların formulanın hansı hissələrinə və hansı ardıcıllıqla tətbiq edilməsindən asılı olmayaraq.
Aksiomlar dəsti yanlış olan (V_1 V_2 ... V_n) siyahısı kimi təmsil olunur. Aksiomlar dəstinə görə F formulanın sübutu, A dəstinə görə doğru olan F-in ACMNF-dən bir termindir. Məsələn, (+(*(+ (*ab))(+ a))c) formulanın (bc) aksiomlarına görə sübutları (* a a) və c terminləridir.
Problem, verilmiş F formulu, A aksiomlar dəsti və k sayı üçün F-in ACMNF-də göründüyü ardıcıllıqla növbəti k sübutları çıxaran sübut generatorunu kodlaşdırmaqdır. Əgər sübutlar tükənərsə, generator F-in ilk sübutundan davam edir. Məsələn, (+(*(+ (*ab))(+ a))c) formulanın (bc) aksiomlarına görə ilk sübutunu yaratmaq (* a a) verir. Üç daha sübut yaratmaq c, (* a a) və c verir. Əgər bir formulanın ACMNF-i oxşar terminlər ehtiva edirsə, 3-cü şəkildəki son nümunədə olduğu kimi, bu terminlər fərqli hesab olunur.
Giriş verilənləri
Standart girişdən məlumat dəstlərini oxuyan sübut generatoru yazın. Məlumat dəstinin məzmunu F A k_1 ... k_n 0, n > 0, burada F bir formula, A aksiomlar dəsti və k_1 ... k_n 0-dan fərqli uzun tam ədədlərdir. Hər bir k_i üçün, i = 1, n, proqram F-in növbəti |k_i| sübutlarını yaradır və əgər k_i > 0 olarsa, bu sübutları standart çıxışda çap edir.
Çıxış verilənləri
Hər çap edilmiş sübut bir sətrin əvvəlindən başlayır və sübutun simvolları arasında boşluqlar yoxdur. Əgər k_i < 0 olarsa, yaradılmış sübutlar çap edilmir. Girişdə boşluqlar sərbəst istifadə olunur. Bir formula ən çox 500 simvola malikdir və ACMNF termini boşluqlar nəzərə alınmadan ən çox 80 simvol uzunluğundadır. Giriş məlumatları faylın sonu ilə tamamlanır və doğrudur.