АЛГОРИТЪМ ЗА ПРЕМИНАВАНЕ КЪМ ОГРАНИЧЕНО ПОЛЗВАНЕ НА ОТРИЦАНИЕ В БЕЗКВАНТОРНИ ФОРМУЛИ
Алгоритъмът започва работата си с произволна дадена безкванторна формула, която в хода на работата се преобразува последователно в други безкванторни формули дотогава, докато се получи формула с ограничено ползване на отрицание. Стъпките, които прави алгоритъмът, могат накратко да бъдат описани по следния начин: с помощта на еквивалентностите за отрицание на true, fail, конюнкция, дизюнкция и отрицание се заменят онези части-подформули на текущата формула, които са такива отрицания и не се съдържат в по-широки такива нейни части. Точната дефиниция на тази замяна може да се даде чрез индукция, съответна на индуктивната дефиниция за безкванторна формула. А именно за всяка безкванторна формула F дефинираме безкванторна формула F ′ (резултат от замяната в F) чрез следните уславяния, където точки 1в, 1г, 2 и 3 важат за всяко цяло число n, по-голямо от 1, и за произволни безкванторни формули F1, …, Fn, а точка 1д - за всяка безкванторна формула F:
0. Ако F е атомарна формула или е някоя от формулите true и fail, то F ′ = F.
1а. Ако F е отрицание на атомарна формула, то F ′ = F.
1б. ( ¬ true ) ′ = fail, ( ¬ fail ) ′ = true.
1в. ( ¬ (F1 & … & Fn) ) ′ = ¬ F1 ∨ … ∨ ¬ Fn .
1г. ( ¬ (F1 ∨ … ∨ Fn) ) ′ = ¬ F1 & … & ¬ Fn .
1д. ( ¬ ¬ F ) ′ = F.
2. (F1 & … & Fn) ′ = F1′ & … & Fn ′.
3. (F1 ∨ … & Fn) ′ = F1′ ∨ … & Fn ′.
Пример 1. Ако A и B са атомарни формули, то
( ( ¬ ¬ A & ¬ B ) ∨ ( ¬ ¬ B & ¬ A ) ) ′ = ( ¬ ¬ A & ¬ B ) ′ ∨ ( ¬ ¬ B & ¬ A ) ′ = ( ( ¬ ¬ A ) ′ & (¬ B ) ′ ) ∨ ( ( ¬ ¬ B ) ′ & ( ¬ A ) ′ ) = (A & ¬ B ) ∨ (B & ¬ A ) .
За произволна безкванторна формула F да дефинираме безкванторните формули F(0), F(1), F(2), … чрез равенствата
F(0) = F, F(k+1) = (F(k)) ′.
Алгоритъмът, за който става дума тук, се състои в това, когато е дадена една безкванторна формула F, да образуваме последователно формулите F(0), F(1), F(2), … дотогава, докато стигнем до естествено число k, за което F(k+1) = F(k). Резултат от работата на алгоритъма е съответната формула F(k).
Пример 2. Нека F е формулата ¬ (A ↔ B), където A и B са атомарни формули. Тогава
F(1) = ¬ (A → B) ∨ ¬ (B → A),
F(2) = ( ¬ ¬ A & ¬ B ) ∨ ( ¬ ¬ B & ¬ A ),
F(3) = (A & ¬ B ) ∨ (B & ¬ A ),
F(4) = F(3).
Следователно резултат от работата на алгоритъма в случая е формулата F(3).
Чрез индукция, съобразена с дефиницията за безкванторна формула, лесно се показва, че F ′ ≡ F за всяка безкванторна формула F и че имаме равенството F ′ = F точно за онези безкванторни формули F, които са с ограничено ползване на отрицание. Следователно при всеки избор на безкванторна формула F и естествено число k формулата F(k) е еквивалентна на F, а равенството F(k+1) = F(k) е налице точно тогава, когато формулата F(k) е с ограничено ползване на отрицание. С индукция относно k се вижда, че за всяко цяло число n, по-голямо от 1,
(F1 & … & Fn)(k) = F1(k) & … & Fn(k),
(F1 ∨ … ∨ Fn)(k) = F1(k) ∨ … ∨ Fn(k)
при всеки избор на безкванторните формули F1, …, Fn и на естественото число k. Това обстоятелство заедно с обстоятелството, че при F(k+1) = F(k) имаме F(l+1) = F(l) за всяко естествено число l, по-голямо от k, позволява чрез индукция, съобразена с дефиницията за безкванторна формула, да докажем, че, която и да е безкванторната формула F, всяко от равенствата F(k+1) = F(k) и ( ¬ F )(k+1) = ( ¬ F )(k) е изпълнено за някое естествено число k (за да можем да твърдим, че алгоритъмът винаги дава резултат, би било достатъчно да установим съществуването на такова число k за първото от двете равенства, но включването и на второто от тях в доказваното твърдение е целесъобразно за провеждането на индукцията).
Последно изменение: 11.06.2004 г.