Streszczenie Logika formalna i predykatowa

Logika Formalna i Logika Predykatów: Kompleksowy Przewodnik dla Studentów

StreszczenieTest wiedzyFiszkiPodcastMapa myśli

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ń (zdanie: jak przepisać zadanie do FOL)

  • Cel: stworzyć formułę w logice predykatów pierwszego rzędu, która dokładnie opisuje tekst zadania.
  • Procedura:
    1. Zidentyfikuj kwantyfikatory: tekst typu „każde”, „wszystkie” → $ orall$, tekst typu „istnieje” → $\exists$.
    2. Określ predykaty/symbole funkcyjne: np. $even(x)$, $odd(x)$, $dir(x)$.
    3. Dodaj warunki (złożone za pomocą $\land$, $\lor$, $\to$, negacji $\neg$) dokładnie tak, jak podaje zadanie.
    4. Kontrola: czytanie formuły na głos często ujawnia błędy.

Definicja: Formułowanie wyrażeń to formuła 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:

  1. Eliminuje się równoważności logiczne i implikacje.
  2. Przesuwa się negacje do wewnątrz za pomocą praw De Morgana i reguły podwójnej negacji.
  3. Zapewnienie, że kwantyfikatory nie dotyczą wzajemnie konfliktujących zmiennych (zmiana nazw zmiennych).
  4. Kwantyfikatory są wyciągane przed formułę.

Skolemizacja (prosta procedura):

  1. Miejmy 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)$.
  2. Po skolemizacji otrzymujemy: $\forall x,P(x,f(x))$ i eliminujemy $\exists$ (funkcja jest stała, więc nie istnieje już kwantyfikator dla $y$).

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: weź 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: weź wiersze, w których wynik wynosi
Zaregistruj se pro celé shrnutí
FiszkiTest wiedzyStreszczeniePodcastMapa myśli
Zacznij za darmo

Masz już konto? Zaloguj się

Logika formalna – przegląd

Klíčové pojmy: Formulace jazyka: identifikujte kvantifikátory a predikáty, Při překladu do FOL napište podmínky do antecedentu a existence/něco do konsekventu: $\\forall...((P)\\to \\exists...)$, PNF: vytáhněte kvantifikátory před formuli po eliminaci implikací a přesunech negací, Skolemizace: $\\exists y$ nahraďte Skolemovou funkcí $f(\cdot)$ závislou na univerzálních proměnných, DNF z řádků s hodnotou 1: konjunkce literálů spojte disjunkcí, CNF z řádků s hodnotou 0: disjunkce literálů spojte konjunkcí, Rezoluce: z $(A\\lor l)$ a $(B\\lor\\neg l)$ odvodíme $(A\\lor B)$, Modus Ponens: z $A$ a $(A\\to B)$ odvodíme $B$, Model: interpretace $(D,\\alpha)$ musí splňovat všechny axiomy, Relace: uspořádání = reflexivní+tranzitivní+antisymetrické; ekvivalence = reflexivní+symetrická+tranzitivní

## 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ń (zdanie: jak przepisać zadanie do FOL) - Cel: stworzyć formułę w logice predykatów pierwszego rzędu, która dokładnie opisuje tekst zadania. - Procedura: 1. Zidentyfikuj kwantyfikatory: tekst typu „każde”, „wszystkie” → $ orall$, tekst typu „istnieje” → $\\exists$. 2. Określ predykaty/symbole funkcyjne: np. $even(x)$, $odd(x)$, $dir(x)$. 3. Dodaj warunki (złożone za pomocą $\\land$, $\\lor$, $\\to$, negacji $\\neg$) dokładnie tak, jak podaje zadanie. 4. Kontrola: czytanie formuły na głos często ujawnia błędy. > Definicja: Formułowanie wyrażeń to formuła 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: 1. Eliminuje się równoważności logiczne i implikacje. 2. Przesuwa się negacje do wewnątrz za pomocą praw De Morgana i reguły podwójnej negacji. 3. Zapewnienie, że kwantyfikatory nie dotyczą wzajemnie konfliktujących zmiennych (zmiana nazw zmiennych). 4. Kwantyfikatory są wyciągane przed formułę. Skolemizacja (prosta procedura): 1. Miejmy 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)$. 2. Po skolemizacji otrzymujemy: $\\forall x\,P(x,f(x))$ i eliminujemy $\\exists$ (funkcja jest stała, więc nie istnieje już kwantyfikator dla $y$). 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: weź 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: weź wiersze, w których wynik wynosi