PROGRAMOWANIE W JĘZYKU LOGIKI – WPROWADZENIE

LOGIKA PIERWSZEGO RZĘDU

Symbole języka pierwszego rzędu. dzielą się na:

a) symbole logiczne (wspólne dla wszystkich języków)

– zmienne przedmiotowe: x, y, z, …

– stałe logiczne:

¬ ∧ ∨ → ↔ ∀ ∃

, , ,

,

,

,

– symbole techniczne: ( , )

b) symbole pozalogiczne (zależne od języka)

– symbole relacyjne: P, Q, R, …

– symbole funkcyjne: f, g, h, …

– stałe przedmiotowe: a, b, c, …

(Symbole pozalogiczne całkowicie określają dany język)

Językiem pierwszego rzędu

nazywamy układ

(

)

L

L

L

L

Con

Fun

l

L

ρ

;

;

;

Re

=

taki, że

–

Re l

L

jest niepustym zbiorem (symboli relacyjnych),

–

Fun

L

jest zbiorem (symboli funkcyjnych),

–

Con

L

jest zbiorem (stałych przedmiotowych),

przy czym zbiory

Re l

L

,

Fun

L

i

Con

L

są rozłączne, natomiast

ρ

L

jest funkcją, która każdemu

symbolowi relacyjnemu i funkcyjnemu przyporządkowuje dodatnią liczbę całkowitą, zwaną

arnością tego symbolu.

Wyróżniamy dwie klasy

wyrażeń sensownych

języka

L

:

a)

termy

– wyrażenia nazwowe,

b)

formuły

– wyrażenia zdaniowe.

Termami

języka

L

nazywamy wyrażenia języka

L

określone przez następujące warunki

indukcyjne:

– wszystkie zmienne i stałe przedmiotowe są termami ,

–

(

)

n

t

t

f

,

,

1

K

jest termem, jeżeli

f

Fun

L

∈

,

( )

ρ

L

f

n

=

oraz

n

t

t

,

,

1

K

są tremami.

Formułami atomowymi

języka

L

nazywamy wyrażenia

(

)

n

t

t

R

,

,

1

K

,

takie że

R

l

L

∈Re

,

( )

ρ

L

R

n

=

a

n

t

t

,

,

1

K

są tremami języka

L

.

Formułami

języka

L

nazywamy wyrażenia języka

L

określone przez następujące warunki

indukcyjne:

– wszystkie formuły atomowe są formułami,

– jeżeli

A

,

B

są formułami, to wyrażenia

( )

¬A

,

(

)

A

B

∧

,

(

)

A

B

∨

,

(

)

A

B

→

,

(

)

A

B

↔

są formułami,

– jeżeli

A

jest formułą i

x

jest zmienną przedmiotową, to wyrażenia

(

)

∀x A

i

( )

∃x A

są formułami.

KLAUZULE

Literał pozytywny

– formuła atomowa (krótko: atom)

Literał negatywny

– negacja atomu

Literał

– literał pozytywny lub negatywny

Klauzula

– formuła postaci

(

)

n

L

L

L

∨

∨

∨

∀

K

2

1

, gdzie

n

i

L

i

,

,

2

,

1

,

K

=

są literałami.

Przykład klauzuli:

( )

( ) ( )

(

)

(

)

a

y

h

x

f

Q

y

x

P

y

x

,

,

,

∨

∀

∀

Klauzula postaci:

(

)

m

k

B

B

A

A

¬

∨

∨

¬

∨

∨

∨

∀

K

K

1

1

jest równoważna formule

(

) (

)

(

)

m

k

B

B

A

A

∧

∧

¬

∨

∨

∨

∀

K

K

1

1

,

która z kolei jest równoważna formule

(

)

k

m

A

A

B

B

∨

∨

→

∧

∧

∀

K

K

1

1

.

Formułę tę zapisujemy w postaci:

4

3

4

2

1

K

4

3

4

2

1

K

przeslanka

m

wniosek

k

B

B

A

A

,

,

,

,

1

1

←

,

przecinki w przesłance (poprzednik implikacji) oznaczają koniunkcje,

przecinki we wniosku (następnik implikacji) oznaczają alternatywy.

Przykład:

klauzula:

( )

( )

(

)

B

y

Q

A

x

P

y

x

∨

¬

∨

¬

∨

∀

∀

zapis:

( )

( )

y

Q

A

B

x

P

,

,

←

Szczególne przypadki klauzul:

1

=

k

Wtedy klauzula jest postaci:

m

B

B

A

,

,

1

K

←

Klauzulę tej postaci nazywamy klauzula

definitywną

.

W szczególności

0

=

m

.

Wtedy po prawej stronie otrzymujemy pustą koniunkcję (brak przesłanek).

Pusta koniunkcja jest zawsze prawdziwa.

Zatem w tym przypadku klauzula jest postaci:

←

A

Prawda

Klauzulę taką nazywamy

jednostkową

.

0

,

0

>

= m

k

.

Wtedy po prawej stronie otrzymujemy pustą alternatywę (brak wniosków).

Pusta alternatywa jest zawsze fałszywa.

Zatem w tym przypadku klauzula jest postaci:

Fałsz

m

B

B

,

,

1

K

←

Klauzulę taką nazywamy

negatywną

.

0

,

0

=

= m

k

.

Wtedy zarówno koniunkcja jak i alternatywa są puste.

Mamy następującą sytuację :

Fałsz

←

Prawda

Zatem w tym przypadku klauzula jest fałszywa.

Nazywamy ja klauzulą

pustą

i oznaczamy

Program w języku logiki.

Programem w języku logiki nazywamy zbiór klauzul postaci:

m

B

B

A

,

,

1

K

←

,

0

≥

n

nagłówek treść, ciało

tzn. klauzul definitywnych (reguł) (

0

>

n

) i klauzul jednostkowych, czyli faktów (

0

=

n

).

Nieformalne znaczenie klauzuli definitywnej

: dla każdego wartościowania zmiennych,

jeżeli

m

i

B

i

,

,

2

,

1

,

K

=

są prawdziwe, to A jest prawdziwe.

Nieformalne znaczenie klauzuli jednostkowej

: A jest prawdziwe dla każdego

wartościowania zmiennych.

Interpretacja

klauzul programu w języku logiki:

m

B

B

A

,

,

1

K

←

,

0

≥

n

a)

deklaratywna (opisowa):

A

jest prawdziwe, jeśli

m

B

B

,

,

1

K

są prawdziwe,

b)

proceduralna (operacyjna): aby rozwiązać

A

rozwiąż

m

B

B

,

,

1

K

.

Definicją predykatu

(relacji, związku, własności)

n

P /

(predykat

P

o

n

argumentach) w

programie w języku logiki

P

nazywamy zbiór wszystkich klauzul, w których nagłówku

występuje

n

P /

.

Program

P

w języku logiki jest opisem obiektów koniecznych do rozwiązania danego

zagadnienia oraz związków jakie zachodzą pomiędzy tymi obiektami.

Program P w języku logiki jednoznacznie określa język pierwszego rzędu

P

L

.

Zadanie do rozwiązania przedstawione jest w postaci tzw.

celu

(ang. goal),

zapytania.

Zapytanie

jest to klauzula negatywna

N

, taka że

P

L

N

∈

.

Wykonanie programu

polega na udowodnieniu, że podany cel wynika logicznie ze zbioru

formuł tworzących program

P

.

W praktyce wykazujemy, że zbiór formuł

P

{ }

N

∪

nie jest spełniany, co w programowaniu w

logice sprowadza się do sprawdzenia, czy ze zbioru formuł

P

{ }

N

∪

można wyprowadzić

klauzulę pustą stosując

regułę rezolucji liniowej

(odpowiadającej stosowaniu bardziej

klasycznych: reguły odrywania i reguły podstawiania).

Jeżeli wykażemy, ze zbiór

P

{ }

N

∪

nie jest spełniany, to ze znanego faktu z logiki

otrzymujemy, że formuła

N

¬

wynika logicznie ze zbioru formuł tworzących program P.

Cel

N

ma postać:

m

B

B

,

,

1

K

←

,

czyli

(

)

Falsz

B

B

m

→

∧

∧

∀

K

1

.

Stąd na podstawie prawa KRZ:

(

)

p

Falsz

p

¬

→

→

mamy :

(

)

(

)

m

B

B

∧

∧

¬

∀

K

1

,

co jest równoważne

(

)

m

B

B

∧

∧

¬∃

K

1

.

Zatem formuła

(

)

m

k

B

B

x

x

∧

∧

∃

∃

K

K

1

1

wynika logicznie z

P

, gdzie

k

x

x

,

,

1

K

są zmiennymi

występującymi w

N

. Tym samym znajdziemy obiekty spełniające cel

N

.

REGUŁA REZOLUCJI ZDANIOWEJ

{

}

{

}

{

}

n

m

n

m

L

L

L

L

L

L

p

L

L

L

p

L

L

L

′

′

′

¬

′

′

′

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

2

1

2

1

2

1

2

1

K

K

K

K

,

n m

,

≥ 0

.

FAKT

Reguła rezolucji zdaniowej jest logiczną regułą wnioskowania, tzn. wniosek reguły rezolucji
zdaniowej wynika ze zbioru przesłanek tej reguły.

REZOLUCJA LINIOWA.

Niech P będzie programem definitywnym.

Reguła rezolucji liniowej

ma postać:

n

m

A

A

A

,

,

,

,

1

K

K

←

– cel

G

k

B

B

B

,

,

1

K

←

– wariant klauzuli

C

programu

P

____________________________________

(

)

σ

n

m

k

m

A

A

B

B

A

A

,

,

,

,

,

,

,

,

1

1

1

1

K

K

K

+

−

←

– nowy cel

gdzie

σ

jest MGU zbioru

{

}

A

B

m

,

, tzn.

A

B

m

σ

σ

=

.

Uzasadnienie:

G

:

(

)

n

m

A

A

A

∧

∧

∧

∧

¬

K

K

1

⇔

n

m

A

A

A

¬

∨

∨

¬

∨

∨

¬

K

K

1

C

:

k

B

B

B

¬

∨

∨

¬

∨

K

1

σ

:

B

A

m

σ

σ

=

Gσ

:

σ

σ

σ

n

m

A

A

A

¬

∨

∨

¬

∨

∨

¬

K

K

1

Cσ

:

σ

σ

σ

k

B

B

B

¬

∨

∨

¬

∨

K

1

___________________________________rezolucja zdaniowa_

σ

σ

σ

σ

σ

σ

n

m

k

m

A

A

B

B

A

A

¬

∨

∨

¬

∨

¬

∨

∨

¬

∨

¬

∨

∨

¬

+

−

K

K

K

1

1

1

1

c

(

)

σ

n

m

k

m

A

A

B

B

A

A

∧

∧

∧

∧

∧

∧

∧

∧

¬

+

−

K

K

K

1

1

1

1