O rachunku zdań mówimy, że jest rozstrzygalny, bo istnieje metoda, która na pytanie

'Czy dana formuła jest spełnialna?'

pozwala uzyskać odpowiedź po skończonej liczbie kroków, niezależnie od tego, czy odpowiedź jest twierdząca, czy przecząca. Chociaż wydaje się, że tak postawione pytanie jest bardzo proste, to zadanie spełnialności formuł rachunku zdań należy do tzw. problemów trudnych informatyki, gdyż wszystkie znane algorytmy rozwiązywania tego problemu mają koszt wykładniczy. Oznacza to, że liczba operacji jakie wykonuje algorytm rozwiązujący to zadanie, wyraża się jako funkcja zależna wykładniczo od rozmiaru formuły. W szczególności, koszt metody zerojedynkowej wyraża się funkcją wykładniczą 2ⁿ, gdzie n jest długością formuły. Jeśli przyjrzymy się tej funkcji, to zauważymy, że nawet dla niezbyt dużych n liczba 2ⁿ jest bardzo duża. Zastosowanie metody zerojedynkowej, dla nieskończenie wielu n nie jest możliwe na najszybszych nawet komputerach, bo czas oczekiwania na wynik byłby niewyobrażalnie długi (por. wykład 4.6).

Problem spełniania, chociaż trudny, jest bardzo ważny w informatyce, ponieważ wiele problemów algorytmicznych (np. problem komiwojażera, problem układania rozkładu zajęć, problem kolorowania grafów itd.) daje się sprowadzić do problemu spełniania. Gdyby istniał tani algorytm rozwiązywania problemu spełniania formuł w rachunku zdań, to można by rozwiązać z małym kosztem i inne problemy.

Zresztą , nie musimy mówić o wielkich problemach, gdyż problem badania prawdziwości formuł jest na porządku dziennym w praktyce informatyki. Testy w programach, to formuły. Od ich prawdziwości zależy działanie algorytmu. Od umiejętnego ustawienia testów zależy struktura, czytelność i nawet czas wykonania naszego programu. Znajomość funktorów logicznych i praw logiki jest więc niezbędna dla każdego informatyka.

Rachunek zdań stanowi ponadto bazę dla rachunku predykatów, o którym będzie mowa w następnym wykładzie.

Uwagi bibliograficzne

Niektóre zdania do analizy logicznej zostały zaczerpnięte ze słownika ortograficznego St. Jodłowskiego i W. Taszyckiego. Przykłady 7.5.1 i 7.5.2 pochodzą podobno od R. Smullyana, a zostały znalezione w książce "The Logical Basis for Computer Programming" Z. Manny i R. Waldingera. Aksjomatyzacja rachunku zdań i przykład dowodu formalnego przedstawiony w punkcie 7.5 pochodzi z książki p. prof. H.Rasiowej "Wstęp do Matematyki Współczesnej".