Andrzej Indrzejczak
HYBRYDOWE SYSTEMY DEDUKCYJNE W LOGIKACH MODALNYCH

1. PRELIMINARIA
1.1 Modalne języki zdaniowe
1.2 Logiki modalne: ujęcie syntaktyczne
1.3 Semantyka relacyjna
1.3.1 Logiki normalne
1.3.2 Pojęcia pomocnicze
1.4 Systemy dedukcyjne, reguły, dowody
2. TYPY SYSTEMÓW DEDUKCYJNYCH
2.1 Rodzaje systemów dedukcyjnych
2.2 Systemy oparte na regule cięcia
2.2.1 Rezolucja
2.2.2 Metoda Davisa / Putnama
2.2.3 Koneksja
2.3 Systemy sekwentowe i tablicowe
2.3.1 Rachunek sekwentów
2.3.2 Systemy tablicowe
2.4 Cięcie a złożoność dowodu
2.5 Próba unifikacji
3. DEDUKCJA NATURALNA W KRZ
3.1 Systemy DN
3.1.1 Kryteria naturalnej dedukcji
3.1.2 Reguły i dowody w DN
3.1.3 System Kalisha / Montague
3.1.4 Adekwatność systemu
3.2 Analityczne wersje DN
3.2.1. KE i DN
3.2.2. System ADN2
4. PRZEGLĄD FORMALIZACJI LOGIK MODALNYCH
4.1 Kryteria wyboru systemów
4.2 Standardowe systemy dedukcyjne
4.2.1 Rachunki sekwentów i systemy tablicowe
4.2.2 Dedukcja naturalna oparta na poddowodach ścisłych
4.2.3 Korespondencja reguł
4.2.4 Ograniczenia standardowego podejścia syntaktycznego
4.2.5 Standardowe formalizacje semantyczne
4.3 Niestandardowe systemy dedukcyjne
4.3.1 Systemy wyższego rzędu
4.3.2 Systemy sekwentów n-arnych (n> 2)
4.3.3 Systemy wielosekwentowe
4.3.4 Systemy poszerzone o nowe strukturalne operacje
5. SYSTEMY ETYKIETOWANE W LOGICE MODALNEJ
5.1 Zastosowanie etykiet
5.2 Podejście zinternalizowane - przypadek logik hybrydowych
5.3 Zewnętrzne zastosowanie etykiet
5.3.1 Minimalna etykietyzacja
5.3.2 Mocna etykietyzacja
5.3.3 Etykietyzacja pośrednia - podejście Fittinga
5.4 Etykietowany system DN
5.4.1 System EDN dla K
5.4.2 Inne logiki normalne
5.4.3 Analityczne wersje EDN
6. LOGIKI LINEARNE
6.1 Sposoby formalizowania linearności
6.1.1 Przegląd proponowanych formalizacji
6.1.2 Porównanie strategii linearyzacji
6.2 System dla S4.3
6.2.1 Reguła charakterystyczna i jej zastosowanie
6.2.2 Efektywność systemu
6.3 EDN dla linearnych logik temporalnych
6.3.1 Formalizacja Kt4.3
6.3.2 Inne logiki linearne
6.4 Pełność analitycznej wersji systemu
7. HYBRYDOWE DN OPARTE NA REZOLUCJI
7.1 Rezolucja i DN w KRZ
7.1.1 DN oparte na klauzulach
7.1.2 System RDN
7.1.3 Symulacja Rezolucji i DP w RDN
7.2 Systemy RDN dla logik modalnych
7.2.1 Modalne RDN bez etykiet dla K
7.2.2 MRDN dla wybranych logik modalnych
7.3 Systemy RDN z etykietami
7.3.1 Etykietowanie lokalne
7.3.2 Etykietowanie globalne
7.3.3 Systemy RDN dla logik hybrydowych
8. KONSTRUKTYWNE DOWODY PEŁNOŚCI
8.1 Automatyczna dedukcja w ADN1-KRZ
8.1.1 Budowanie zbiorów Hintikki
8.1.2 Algorytmy dla ADN1
8.1.3 Optymalizacja
8.2 Pełność EADN1 - logiki nielinearne
8.2.1 Etykietowane zbiory Hintikki
8.2.2 Procedury stałe
8.2.3 Logiki nietranzytywne i niesymetryczne
8.2.4 Optymalizacja
8.2.5 Logiki tranzytywne i kontrola pętli
8.2.6 Nietranzytywne logiki symetryczne i euklidesowe
8.2.7 Tranzytywne logiki symetryczne i euklidesowe
8.3 Logiki linearne
8.3.1 Poszerzanie łańcucha
8.3.2 Algorytm szukania dowodu
8.3.3 Analiza najgorszego przypadku


Wydawnictwo: Uniwersytet Łódzki
Rok wydania: 2006, wyd.I
Stron: 290
Okładka: miękka
Stan ogólny: BDB, zdjęcie powyżej
Dodatkowe uwagi: książka nowa