Scan0024

32 Metoda rezolucji. Elementy logiki pierwszego rzędu

2. Tworzymy postać klauzulową:

5		- r,	s},{~ q,	~^1},{p}}
Przeprowadzamy dowód:
1.		6.		s} i, 4
2.	{~p,r}	7.	{~p,s}	2, 3
3.	{~ r, s}	8.	{-4	5, 6
4.	q, ~ s}	9.		5, 7
5.	M	10.	□	8, 9

Poniważ otrzymaliśmy klauzulę pustą, zatem wnioskowanie jest poprawne.

3.2 Elementy logiki pierwszego rzędu

W logice pierwszego rzędu (rachunku kwantyfikatorów, rachunku funkcyjnym) stosujemy:

•    x,y, z — zmienne indywiduowe (indywidua) — reprezentujące dowolne przedmioty,

•    a, b, c — stale indywiduowe — reprezentujące ustalone przedmioty,

•    P,Q,R — symbole predykatowe lub predykatywne (predykaty) — opisujące własności zmiennych lub relacje (związki) zachodzące pomiędzy zmiennymi,

• f\ lub V (for Ali) — kwantyfikator ogólny (generalny, duży) czytany ⁷⁷dla każdego ”,

1

   V lub 3 (Exists) — kwantyfikator szczegółowy (egzystencjalny, mały) czytany ⁷⁷istnieje taki, że”,

•    funktory zdaniotwórcze, • nawiasy.