Logika matematyczna w informatyce

Książka ta jest poświęcona zagadnieniom logiki, które stanowią podstawę wykształcenia każdego informatyka i inżyniera stosującego metody komputerowe.
Omówiono w niej rachunek zdań, logikę pierwszego rzędu, programowanie w logice, specyfikację i weryfikację programów oraz logikę temporalną. Wszystkie przedstawione implementacje wykonano w języku Prolog.
Jest to doskonały podręcznik, o wielkich walorach dydaktycznych, napisany z dużym znawstwem tematu, a na dodatek zrozumiale. W każdym rozdziale podano wiele przykładów ilustrujących omawiane pojęcia i metody, a także zamieszczono ćwiczenia o zróżnicowanym stopniu trudności.
Książka jest przeznaczona dla studentów pierwszych lat studiów na kierunkach informatycznych. Skorzystają z niej także pracownicy dydaktyczni prowadzący zajęcia z logiki stosowanej.

Spis treści

Przedmowa

1. Wprowadzenie

1.1. Początki logiki matematycznej
1.2. Rachunek zdań
1.3. Rachunek predykatów
1.4. Dowodzenie twierdzeń i programowanie w logice
1.5. Systemy logiczne
1.6. Ćwiczenie

2. Rachunek zdań: formuły, modele, tabele semantyczne

2.1. Operatory logiczne
2.2. Formuły rachunku zdań
2.3. Interpretacje
2.4. Logiczna równoważność
2.5. Spełnialność, prawdziwość i konsekwencje logiczne
2.6. Metoda tabel semantycznych
2.7. Poprawność i pełność
2.8. Implementacja w Prologu
2.9. Ćwiczenia

3. Rachunek zdań: systemy dowodzenia

3.1. Wyprowadzanie formuł
3.2. System gentzenowski
3.3. System hilbertowski
3.4. Poprawność i pełność systemu hilbertowskiego
3.5. Weryfikator dowodów w Prologu
3.6. Odmiany systemów dowodzenia*
3.7. Ćwiczenia

4. Rachunek zdań: rezolucja i diagramy binarnych decyzji

4.1. Rezolucja
4.2. Diagramy binarnych decyzji (DBD)
4.3. Algorytmy operujące na diagramach binarnych decyzji
4.4. Złożoność*
4.5. Ćwiczenia

5. Rachunek predykatów: formuły, modele, tabele semantyczne

5.1. Relacje i predykaty
5.2. Formuły rachunku predykatów
5.3. Interpretacje
5.4. Logiczna równoważność
5.5. Metoda tabel semantycznych
5.6. Implementacja w Prologu
5.7. Modele skończone i nieskończone*
5.8. Rozstrzygalność*
5.9. Ćwiczenia

6. Rachunek predykatów: systemy dowodzenia

6.1. System gentzenowski
6.2. System hilbertowski
6.3. Implementacja w Prologu
6.4. Teorie zupełne i rozstrzygalne*
6.5. Ćwiczenia

7. Rachunek predykatów: rezolucja

7.1. Funkcje i termy
7.2. Postać klauzulowa formuł
7.3. Modele Herbranda
7.4. Twierdzenie Herbranda*
7.5. Rezolucja dla klauzul ustalonych
7.6. Podstawienia
7.7. Uzgadnianie
7.8. Rezolucja
7.9. Ćwiczenia

8. Programowanie w logice

8.1. Formuły jako programy
8.2. SLD-rezolucja
8.3. Prolog
8.4. Programowanie współbieżne w logice*
8.5. Programowanie w logice z więzami*
8.6. Ćwiczenia

9. Programy: semantyka i weryfikacja

9.1. Wprowadzenie
9.2. Semantyka języków programowania
9.3. System dowodzenia HL
9.4. Weryfikacja programów
9.5. Synteza programów
9.6. Poprawność i pełność systemu HL
9.7. Ćwiczenia

10. Programy: formalne specyfikacje w notacji Z

10.1. Przykład: sygnalizator świetlny
10.2. Notacja Z
10.3. Przykład: tabela semantyczna
10.4. Ćwiczenia

11. Logika temporalna: formuły, modele, tabele semantyczne

11.1. Wprowadzenie
11.2. Składnia i semantyka
11.3. Modele czasu
11.4. Metoda tabel semantycznych
11.5. Implementacja metody tabel semantycznych w Prologu
11.6. Ćwiczenia

12. Logika temporalna: systemy dowodzenia i zastosowania

12.1. System dowodzenia L
12.2. Poprawność i pełność L*
12.3. Inne logiki temporalne*
12.4. Specyfikacje oraz weryfikacja programów*
12.5. Weryfikacja przez model*
12.6. Ćwiczenia

A. Teoria mnogości
A.1. Zbiory skończone i nieskończone
A.2. Operacje na zbiorach
A.3. Zbiory uporządkowane
A.4. Relacje i funkcje
A.5. Moc zbioru
A.6. Dowodzenie właściwości zbiorów

B. Dalsze lektury

Bibliografia
Wykaz symboli
Skorowidz