Генератор Доказів#1401

Генератор Доказів

1 секунда

64 мегабайти

Дуже складна

Логічна формула має синтаксис, показаний на рисунку 1(a), де змінна позначає значення істинності. Формула $(\textbf{+ F_1 \ldots F_n})$ позначає логічну диз'юнкцію формул $\textbf{F_i}$ , $(\textbf{* F_1 \ldots F_n})$ позначає логічну кон'юнкцію формул $\textbf{F_i}$ , а $F$ — це заперечення $F$ . Якщо формула має специфічний синтаксис, заданий на рисунку 1(b), кажуть, що формула знаходиться в ACM-нормальній формі (ACMNF).

\includegraphics{https://static.e-olymp.com/content/12/120a1d7fd9315cf5058abcec7b190e997db84ee9.jpg}

Формула перетворюється у ACMNF за допомогою наведених нижче правил переписування, де $F$ позначає формулу, $S$ — непорожню послідовність формул, а $s$ і $s’$ — можливо, порожні послідовності формул. Застосування правила переписування $q \to r$ \textbf{q} \rightarrow \textbf{r} до формули $F$ означає заміну частини $F$ , що відповідає шаблону $q$ , на $r$ , як показано на рисунку 2. Перетворення завершується, коли жодне правило більше не може бути застосоване. Перетворення завершиться для будь-якої формули, і результат унікальний незалежно від порядку застосування правил і вибраних частин формули.

\includegraphics{https://static.e-olymp.com/content/60/6050aee4925c3544de7f551b99e942b6dc8de22f.jpg}

Набір аксіом подається як список $(\textbf{V_1} \textbf{V_2} \ldots \textbf{V_n})$ хибних значень. Доведенням формули $F$ щодо множини аксіом $A$ називається терм із ACMNF для $F$ , який істинний відносно $A$ . Наприклад, терми $(* a a)$ та $c$ є доведеннями формули $(+(*(+ (*ab))(+ a))c)$ відносно аксіом $(bc)$ .

Завдання полягає у написанні генератора доведень, який для заданої формули $F$ , множини аксіом $A$ та чисел $k_{1}, \dots, k_{n}$ k_1, \ldots, k_n виводить наступні $k$ доведень формули $F$ у тому порядку, в якому вони зустрічаються у ACMNF для $F$ . Якщо доведення закінчуються, генератор продовжує з першого доведення формули $F$ . Наприклад, генерація першого доведення формули $(+(*(+ (*ab))(+ a))c)$ відносно аксіом $(bc)$ дає $(* a a)$ . Три наступних доведення: $c$ , $(* a a)$ , $c$ . Якщо у ACMNF формули зустрічаються схожі (але різні за формою) терми, як у останньому прикладі на рисунку 3, такі терми вважаються різними.

Вхідні дані

Напишіть генератор доведень, який зчитує набори даних зі стандартного вводу. Вміст одного набору даних: $\textbf{F}\ \textbf{A}\ \textbf{k_1}\ \ldots\ \textbf{k_n}\ 0$ , де $n > 0$ n > 0, $F$ — формула, $A$ — набір аксіом, а $\textbf{k_1}, \ldots, \textbf{k_n}$ — цілі числа (long integer), які відмінні від $0$ . Для кожного $\textbf{k_i}$ , $i = 1, \dots, n$ i=1, \ldots, n, програма генерує наступні $|\textbf{k_i}|$ доведень формули $F$ і, якщо $\textbf{k_i} > 0$ , виводить ці доведення у стандартний вивід.

Вихідні дані

Кожне виведене доведення починається з початку рядка, і між символами доведення немає пропусків. Згенеровані доведення не виводяться, якщо $\textbf{k_i} < 0$ . Пробіли у вхідних даних можуть використовуватися довільно. Довжина формули — не більше $500$ символів, а терм ACMNF — не більше $80$ символів (без пропусків). Вхідні дані закінчуються кінцем файлу і є коректними.

Приклади

Приклад 1