Streszczenie Logika formalna i predykatowa
Logika Formalna i Logika Predykatów: Kompleksowy Przewodnik dla Studentów
Wstęp
Logika formalna to zbiór metod i notacji służących do precyzyjnego wyrażania twierdzeń o obiektach, relacjach i dowodach. Celem niniejszego materiału jest przedstawienie przystępnego przeglądu podstawowych zagadnień, procedur i przydatnych sztuczek pojawiających się w zadaniach z logiki formalnej (np. formułowanie języka, skolemizacja, PNF, rezolucja, modus ponens, modele teorii). Materiał został zaprojektowany do samodzielnej nauki i ma na celu ułatwienie orientacji oraz przygotowania do ćwiczeń lub egzaminu.
Podstawowe części i procedury
Poniżej rozłożymy często powtarzające się zadania na mniejsze kroki, uzupełnimy definicje, przykłady i praktyczne wskazówki.
1) Formułowanie wyrażeń (przekształcanie zadań na język FOL)
- Cel: stworzyć formułę w logice predykatów pierwszego rzędu, która dokładnie opisuje tekst zadania.
- Procedura:
- Zidentyfikuj kwantyfikatory: tekst typu „każde”, „wszystkie” → $ orall$, tekst typu „istnieje” → $\exists$.
- Określ predykaty/symbole funkcyjne: np. $even(x)$, $odd(x)$, $dir(x)$.
- Dodaj warunki (złożone za pomocą $\land$, $\lor$, $\to$, negacji $\neg$) dokładnie tak, jak podaje zadanie.
- Kontrola: czytanie formuły na głos często ujawnia błędy.
Definicja: Formułowanie wyrażeń to proces tworzenia formuły logiki predykatów, która za pomocą kwantyfikatorów i predykatów dokładnie oddaje twierdzenie w języku naturalnym.
Praktyczny przykład: „Między każdymi dwoma różnymi liczbami parzystymi istnieje liczba nieparzysta.”
- Krok 1: dwie zmienne → $ orall x\forall y$.
- Krok 2: obie parzyste: $even(x)\land even(y)$.
- Krok 3: różne i uporządkowanie: $x<y$ (lub $x\neq y$ zgodnie z zadaniem).
- Krok 4: istnienie nieparzystej między nimi: $\exists z,(odd(z)\land x<z\land z<y)$.
- Wynikowa formuła: $$\forall x\forall y,\bigl((even(x)\land even(y)\land x<y)\to \exists z,(odd(z)\land x<z\land z<y)\bigr)$$
Wskazówka: W większości zdań obowiązuje, że części z $\forall$ wprowadzają założenia i kształt implikacji $(P\to Q)$, gdzie $P$ to warunki dotyczące zmiennych, a $Q$ to istnienie lub inny warunek końcowy.
Ciekawostka: W praktyce czasem nie można automatycznie uzupełnić sygnatury o nowe predykaty; jeśli w zadaniu masz tylko $dir(x)$ (katalog), ale potrzebujesz „pliku”, można go modelować jako $\neg dir(x)$, jeśli jest to rozsądne w kontekście.
2) Prenexowa postać normalna (PNF) i Skolemizacja
- Cel PNF: przenieść wszystkie kwantyfikatory przed samą formułę, bez zmiany znaczenia (z wyjątkiem zmiennych wolnych).
- Skolemizacja: usunięcie kwantyfikatorów egzystencjalnych poprzez wprowadzenie funkcji Skolema, aby uzyskać równoważną formułę odpowiednią do rezolucji.
Podstawowa procedura PNF:
- Eliminuje się równoważności logiczne i implikacje.
- Przesuwa się negacje do wewnątrz za pomocą praw De Morgana i reguły podwójnej negacji.
- Zapewnia się, że kwantyfikatory nie wiążą zmiennych, które mogłyby ze sobą kolidować (poprzez zmianę ich nazw).
- Kwantyfikatory są wyciągane przed formułę.
Skolemizacja (prosta procedura):
- Rozważmy formułę w PNF: $\forall x\exists y,P(x,y)$. Aby usunąć $\exists y$, wprowadzamy funkcję Skolema $f(x)$ i zastępujemy $y$ wyrażeniem $f(x)$.
- Po skolemizacji otrzymujemy: $\forall x,P(x,f(x))$ i eliminujemy $\exists$ (zmienna $y$ jest zastępowana termem Skolema).
Przykład (krótko): $$\forall x\exists y,R(x,y)$$ Skolemizacja → $$\forall x,R(x,f(x))$$
3) CNF i DNF (konwersja między nimi)
- DNF (dysjunkcyjna postać normalna): dysjunkcja koniunkcji literałów; odpowiednia, gdy chcemy bezpośrednio odczytywać prawdziwe wiersze tabeli prawdy.
- CNF (koniunkcyjna postać normalna): koniunkcja dysjunkcji literałów; odpowiednia dla dowodów rezolucyjnych.
Konwersja z tabeli prawdy:
- DNF: bierzemy wiersze, w których wynik wynosi 1; dla każdego takiego wiersza utwórz koniunkcję literałów (zmienna jest zanegowana, jeśli w wierszu ma 0). Na koniec połącz te koniunkcje dysjunkcją.
- CNF: bierzemy wiersze, w który
Zarejestruj się po pełne podsumowanieMasz już konto? Zaloguj się
Logika formalna – przegląd
Klíčové pojmy: Formułowanie języka: identyfikuj kwantyfikatory i predykaty, Przy tłumaczeniu na FOL zapisz warunki w antecedensie, a wyrażenia egzystencjalne w konsekwensie: $\\forall...((P)\\to \\exists...)$, PNF: przenieś kwantyfikatory przed formułę po eliminacji implikacji i przesunięciu negacji, Skolemizacja: zastąp $\\exists y$ funkcją Skolema $f(\cdot)$ zależną od zmiennych uniwersalnych, DNF z wierszy z wartością 1: połącz koniunkcje literałów dysjunkcją, CNF z wierszy z wartością 0: połącz dysjunkcje literałów koniunkcją, Rezolucja: z $(A\\lor l)$ i $(B\\lor\\neg l)$ wyprowadzamy $(A\\lor B)$, Modus Ponens: z $A$ i $(A\\to B)$ wyprowadzamy $B$, Model: interpretacja $(D,\\alpha)$ musi spełniać wszystkie aksjomaty, Relacje: porządek = refleksywna + przechodnia + antysymetryczna; równoważność = refleksywna + symetryczna + przechodnia