M ETODY D OWODZENIA T WIERDZE ´N I A UTOMATYZACJA R OZUMOWA ´N

(1)

M ^ETODY D ^OWODZENIA T ^{WIERDZE ´} ^N I A UTOMATYZACJA R ^{OZUMOWA ´} ^N

K

ONWERSATORIUM

5:

T

ABLICE

A

NALITYCZNE

V rok kognitywistyki UAM

1 Reguły

1.1 KRZ

Reguły rozszerzania tablic analitycznych dla formuł bez kwantyfikatorów (dla j˛e- zyka KRZ) zapisanych w notacji Smullyana s ˛a nast˛epuj ˛ace:

¬¬ψ ψ

¬>

⊥

¬ ⊥

>

α α1

α₂

β

HH β1 β2

Cwiczenie. Zapisz reguły dla α-formuł oraz β-formuł w przypadku poszczegól-´ nych funktorów prawdziwo´sciowych oraz ich negacji.

Przypominamy tabel˛e składników formuł, zapisanych w jednolitej notacji:

α α1 α2

ϕ ∧ ψ ϕ ψ

¬(ϕ ∨ ψ) ¬ϕ ¬ψ

¬(ϕ → ψ) ϕ ¬ψ

¬(ϕ ← ψ) ¬ϕ ψ

¬(ϕ ↑ ψ) ϕ ψ

ϕ ↓ ψ ¬ϕ ¬ψ

ϕ 9 ψ ϕ ¬ψ

ϕ 8 ψ ¬ϕ ψ

β β1 β2

¬(ϕ ∧ ψ) ¬ϕ ¬ψ

ϕ ∨ ψ ϕ ψ

ϕ → ψ ¬ϕ ψ

ϕ ← ψ ϕ ¬ψ

ϕ ↑ ψ ¬ϕ ¬ψ

¬(ϕ ↓ ψ) ϕ ψ

¬(ϕ 9 ψ) ¬ϕ ψ

¬(ϕ 8 ψ) ϕ ¬ψ

(2)

1.2 KRP

W przypadku j˛ezyków pierwszego rz˛edu, dodajemy nast˛epuj ˛ace reguły rozszerzania tablic analitycznych (w notacji Smullyana):

γ γ(t)

(dla dowolnego termu zamkni˛etego j˛ezyka L^par)

δ δ(a)

(dla dowolnego nowego parametru a)

Przypominamy jednolit ˛a notacj˛e dla formuł z kwantyfikatorami:

γ γ(t) δ δ(t)

∀xϕ ϕ(x/t) ∃xϕ ϕ(x/t)

¬∃xϕ ¬ϕ(x/t) ¬∀xϕ ¬ϕ(x/t)

2 Wskazówki heurystyczne

Propozycja notacji podana została na wykładzie. Je´sli budzi jakie´s w ˛atpliwo´sci, prosz˛e pyta´c. Rozwa˙zane dalej przykłady powinny by´c pomocne w rozumieniu tej notacji oraz sprawnym posługiwaniu si˛e ni ˛a.

Kolejno´s´c kroków budowania tablicy: (o ile to mo˙zliwe, to) najpierw reguły nierozgał˛eziaj ˛ace, potem rozgał˛eziaj ˛ace.

Oszcz˛edzanie niepotrzebnej pracy: je´sli uzyskała´s na której´s gał˛ezi budowanej tablicy analitycznej par˛e formuł wzajem sprzecznych (lub ⊥), to zamknij t˛e gał ˛a´z.

3 Dowody tablicowe

3.1 W KRZ

1. Zbudujemy tablice analityczne:

1. dla formuły (p → q) → ¬(p → ¬q) oraz

2. dla zaprzeczenia tej formuły, tj. dla formuły ¬((p → q) → ¬(p → ¬q)).

Tablica analityczna dla (p → q) → ¬(p → ¬q):

(3)

(p → q) → ¬(p → ¬q) ^1.^→

H HH HH H (1_l) ¬(p → q) ^2.^¬→

(2g) p (2d) ¬q

◦1

(1_p) ¬(p → ¬q) ^3.^¬→

(3g) p (3d) ¬¬q ^4.^¬¬

(4) q

◦₂

Tablica analityczna dla ¬((p → q) → ¬(p → ¬q)):

¬[(p → q) → ¬(p → ¬q)] ^1.^¬→

(1g) p → q ^3.^→ (1_d) ¬¬(p → ¬q) ^2.^¬¬

(2) p → ¬q ^4.^→

HH HH HH H

(3l) ¬p

HH HH (4l) ¬p

◦1

(4p) ¬q

◦2

(3p) q

HH HH (4l) ¬p

◦3

(4p) ¬q

×3_p,4_p

Zadna z tych tablic nie jest, jak wida´c, sprzeczna (zamkni˛eta).˙ 2. Zbudujemy dowód tablicowy prawa modus ponendo ponens:

((ϕ → ψ) ∧ ϕ) → ψ

Konstruujemy zatem tablic˛e, w której korzeniu umieszczamy zaprzeczenie for- muły ((ϕ → ψ) ∧ ϕ) → ψ:

(4)

¬(((ϕ → ψ) ∧ ϕ) → ψ) ^1.^¬→

(1g) (ϕ → ψ) ∧ ϕ ^2.^∧ (1d) ¬ψ

(2g) ϕ → ψ ^3.^→ (2d) ϕ

HH HH (3l) ¬ϕ

×2_d,3_l

(3p) ψ

×1_d,3_p

Tablica jest sprzeczna, a wi˛ec ((ϕ → ψ) ∧ ϕ) → ψ jest tez ˛a tablicow ˛a.

3. Zbudujemy tablic˛e analityczn ˛a dla zbioru:

S = {p ∧ ¬r, p → q, q → r}.

(0.1) p ∧ ¬r ^1.^∧ (0.2) p → q ^2.^→ (0.3) q → r ^3.^→

(1g) p (1d) ¬r

H HH HH (2l) ¬p

×1g,2_l

(2p) q

HH HH (3l) ¬q

×2_p,3_l

(3p) r

×1_d,3_p

4. Zbudujemy tablic˛e analityczn ˛a dla zbioru:

S = { (p → q) → r, ¬(r ∨ s), (p → q) ∨ t, t → (r ∨ q) }.

(5)

(0.1) (p → q) → r ^2.^→ (0.2) ¬(r ∨ s) ^1.^¬∨

(0.3) (p → q) ∨ t ^3.^∨ (0.4) t → (r ∨ q) ^4.^→

(1g) ¬r (1d) ¬s

HH HH HH HH HH

(2_l) ¬(p → q) ^5.^¬→

HH HH HH H

(3l) p → q

×2_l,3_l

(3p) t

H HH HH (4_l) ¬t

×₃_p_,4_l

(4p) r ∨ q ^6.^∨ (5g) p (5d) ¬q

HH H H (6l) r

×1_g,6_l

(6p) q

×5_g,6_p

(2p) r

×1_g,2_p

5. Ustalimy czy wniosek wynika tablicowo z przesłanek:

p → q r → s (p ∨ q) → (r ∨ s)

Budujemy zatem tablic˛e analityczn ˛a, rozpoczynaj ˛ac j ˛a od przesłanek oraz za- przeczonego wniosku:

(6)

(0.1) p → q^5.^→ (0.2) r → s^3.^→ (0.3) ¬((p ∨ q) → (r ∨ s))^1.^¬→

(1_g) p ∨ q^4.^∨ (1d) ¬(r ∨ s)^2.^¬→

(2g) ¬r (2_d) ¬s

HH H HH HH

(3_l) ¬r

HH HH HH (4l) p

HH H (5l) ¬p

×4_l,5_l

(5p) q

◦1

(4p) q

HH H (5l) ¬p

◦2

(5p) q

◦3

(3_p) s

×2_g,3_p

Tablica nie jest zamkni˛eta, a wi˛ec wniosek nie wynika tablicowo z przesłanek.

3.2 W logice pierwszego rz˛edu

1. Zbudujemy tablic˛e analityczn ˛a dla zbioru zda´n: { ∃x∃y ((P (x) ∧ ¬P (y)) ∧

¬Q(x, y)), ∀x∀y ((P (x) ∧ R(y)) → Q(x, y)), ¬∃x (¬P (x) ∧ ¬R(x)) }.

(7)

∃x∃y ((P (x) ∧ ¬P (y)) ∧ ¬Q(x, y)) ^1.

√

a

∀x∀y ((P (x) ∧ R(y)) → Q(x, y)) ^6.^?^a

¬∃x (¬P (x) ∧ ¬R(x)) ^5.^?^b (1) ∃y ((P (a) ∧ ¬P (y)) ∧ ¬Q(a, y)) ^2.

√

b

(2) ((P (a) ∧ ¬P (b)) ∧ ¬Q(a, b)) ^3.∧

(3_g) P (a) ∧ ¬P (b) ^4.^∧ (3_d) ¬Q(a, b)

(4g) P (a) (4d) ¬P (b)

(5) ¬(¬P (b) ∧ ¬R(b)) ^8.^¬∧

(6) ∀y ((P (a) ∧ R(y)) → Q(a, y)) ^7.^?^b (7) (P (a) ∧ R(b)) → Q(a, b) ^11.^→

HH HH HH HH HH H

(8l) ¬¬P (b) ^9.^¬¬

(9) P (b)

×₄_d_,9

(8p) ¬¬R(b) ^10.^¬¬

(10) R(b)

H HH HH HH

(11l) ¬(P (a) ∧ R(b)) ^12.^¬∧

HH HH H (12l) ¬P (a)

×4g,12_l

(12p) ¬R(b)

×10,12p

(11_p) Q(a, b)

×3_d,11_p

Zauwa˙zmy, ˙ze (na mocy prawa De Morgana) ¬∃x (¬P (x) ∧ ¬R(x)) jest rów- nowa˙zne zdaniu ∀x (P (x) ∨ R(x)).

Niech predykat P b˛edzie dumnie interpretowany jako własno´s´c bycia Pola- kiem, R jako własno´s´c bycia obcokrajowcem, za´s Q(x, y) interpretujmy jako x szydzi zy. Otrzymujemy wtedy nast˛epuj ˛ace brednie:

(8)

Pewien Polak nie szydzi z co najmniej jednego Niepolaka. Ka˙zdy Polak szydzi ze wszystkich obcokrajowców. Nikt nie jest jednocze´snie Niepo- lakiem oraz nieobcokrajowcem.

Po zastosowaniu prawa De Morgana do ostatniego z tych zda´n otrzymujemy zgrabniejszy stylistycznie, ale w dalszym ci ˛agu sprzeczny tekst:

Pewien Polak nie szydzi z kogo´s, kto Polakiem nie jest. Wszyscy Polacy szydz ˛a z ka˙zdego obcokrajowca. Ka˙zdy jest Polakiem lub obcokrajowcem.

2. Ustalimy czy wniosek wynika tablicowo z przesłanek:

∀x (P (x) → Q(x))

∃y (R(y) ∧ Q(y))

∀z (P (z) → R(z))

∀x (P (x) → Q(x)) ^2.^?^{a 4.}^?^b

∃y (R(y) ∧ Q(y)) ^1.

√ a

¬∀z (P (z) → R(z)) ^3.

√ b

(1) R(a) ∧ Q(a)^5.^∧ (2) P (a) → Q(a) ^8.^→ (3) ¬(P (b) → R(b)) ^6.^¬→

(4) P (b) → Q(b) ^7.^→ (5g) R(a) (5d) Q(a) (6g) P (b) (6d) ¬R(b)

HH HH H

(7_l) ¬P (b)

×₆_g_,7_l

(7p) Q(b)

HH H

(8l) ¬P (a)

♣

(8p) Qa

♠

(9)

Tablica nie jest zamkni˛eta, a zatem wniosek nie wynika tablicowo z przesła- nek. Otwarte gał˛ezie tablicy pozwalaj ˛a zbudowa´c modele, w których prawdziwe s ˛a przesłanki, a fałszywy jest wniosek:

♣ P Q R

a – + +

b + + –

♠ P Q R

a ? + +

b + + –

Ta notacja powinna by´c oczywista, dla przykładu:

1. Znak + na przeci˛eciu kolumny dla P oraz wiersza dla b w drugiej z tych tabelek oznacza, ˙ze na gał˛ezi ♠ znajduje si˛e zdanie atomowe P (b).

2. Znak − na przeci˛eciu kolumny dla R oraz wiersza dla b w drugiej z tych tabelek oznacza, ˙ze na gał˛ezi ♠ znajduje si˛e zdanie atomowe ¬R(b).

3. Znak ? na przeci˛eciu kolumny dla P oraz wiersza dla a w drugiej z tych tabelek oznacza, ˙ze na gał˛ezi ♠ nie ma ani zdania atomowego P (a) ani zdania atomowego ¬P (a).

Zauwa˙zmy ponadto, ˙ze pierwsza przesłanka jest formuł ˛a typu γ, a wi˛ec nale-

˙zało zastosowa´c do niej stosown ˛a reguł˛e zarówno dla stałej a, jak i dla stałej b.

3. Ostatni walczyk w Mi˛edzyzdrojach. Czy z przesłanek:

Ka˙zdy kogo´s lubi. Niektórzy lubi ˛a tylko tych, którzy ich nie lubi ˛a.

wynika tablicowo wniosek: Kto´s jest lubiany przez niesamoluba.?

Znajdujemy struktur˛e składniow ˛a przesłanek i wniosku. Wyst˛epuje tu tylko jeden predykat: czytajmy L(x, y) jako x lubi y. Wtedy oczywi´scie L(x, x) czytamy:

x lubi siebie (przyjmijmy, ˙ze jest to równoznaczne z x jest samolubem). Badane wnioskowanie przebiega według nast˛epuj ˛acego schematu:

∀x∃y L(x, y)

∃x∀y (L(x, y) → ¬L(y, x))

∃x∃y (L(y, x) ∧ ¬L(y, y))

(10)

∀x∃y L(x, y) ^2.^?^a

∃x∀y (L(x, y) → ¬L(y, x)) ^1.

√ a

¬∃x∃y (L(y, x) ∧ ¬L(y, y)) ^5.^?^b (1) ∀y(L(a, y) → ¬L(y, a)) ^4.^?^{a 6.}^?^b

(2) ∃y L(a, y) ^3.

√ b

(3) L(a, b)

(4) L(a, a) → ¬L(a, a) ^10.^→ (5) ¬∃y (L(y, b) ∧ ¬L(y, y)) ^7.^?^a

(6) L(a, b) → ¬L(b, a) ^8.^→ (7) ¬(L(a, b) ∧ ¬L(a, a)) ^9.^¬∧

HH HH HH H

(8l) ¬L(a, b)

×_3,8_l

(8p) ¬L(b, a)

H HH HH H

(9l) ¬L(a, b)

×3,9_l

(9p) ¬¬L(a, a)

H HH H H

(10l) ¬L(a, a)

×9,10_l

(10p) ¬L(a, a)

×9,10p

Tablica jest zamkni˛eta, a zatem wniosek wynika tablicowo z przesłanek.

4. Zbudujemy tablic˛e analityczn ˛a dla zbioru formuł:

{P (a), ¬Q(a), ∀x(P (x) → (R(x) ∨ S(x))), ¬S(a),

∀x((R(x) ∧ T (x)) → Q(x)), ¬∃x(R(x) ∧ ¬T (x))}.

(11)

(0.1) P (a) (0.2) ¬Q(a)

(0.3) ∀x(P (x) → (R(x) ∨ S(x)))^1.^?^a (0.4) ¬S(a)

(0.5) ∀x((R(x) ∧ T (x)) → Q(x))^2.^?^a (0.6) ¬∃x(R(x) ∧ ¬T (x))^3.^?^a

(1) (P (a) → (R(a) ∨ S(a)))^4.^→ (2) ((R(a) ∧ T (a)) → Q(a))^5.^→

(3) ¬(R(a) ∧ ¬T (a))

HH HH HH HH HH H

(4l) ¬P (a)

×0.1,4_l

(4p) R(a) ∨ S(a)^6.^→

HH HH HH

(5l) ¬(R(a) ∧ ¬T (a))^7.^¬∧

H HH HH HH

(6l) R(a)

HH HH H

(7l) ¬R(a)

×6_l,7_l

(7p) ¬T (a)

HH H

(8l) ¬R(a)

×6_l,8_l

(8p) ¬¬T (a)

×7_p,8_p

(6p) S(a)

×0.4,6_p

(5p) Q(a)

×_0.2,5_p

Tablica zamkni˛eta. Zauwa˙zmy, ˙ze poniewa˙z w zdaniach naszego zbioru wyst˛e- powała stała a, wi˛ec nale˙zało dla niej zastosowa´c reguł˛e dla wszystkich γ-formuł w tablicy.

5. Spróbujemy zbudowa´c tablic˛e analityczn ˛a dla zbioru zda´n:

{ ∀x(P (x) → Q(x)), ∀x∃y(R(y) ∧ S(y, x)), ∀x((R(x) ∧ Q(x)) → T (x)),

∀x∀y((T (y) ∧ S(y, x)) → T (x)), ¬∀x∀y((¬P (y) → ¬S(x, y)) → T (x))}.

(12)

∀x (P (x) → Q(x))^4.^?^{a 5.}^?^b

∀x∃y (R(y) ∧ S(y, x))^6.^?^{a 7.}^?^b

∀x ((R(x) ∧ Q(x)) → T (x))^8.^?^{a 9.}^?^b

∀x∀y ((T (y) ∧ S(y, x)) → T (x))^10.^?^{a 11.}^?^b

¬(∀x∀y ((¬P (y) → ¬S(x, y)) → T (x)))^1.

√ a

(1) ¬∀y ((¬P (y) → ¬S(a, y)) → T (a))^2.

√ b

(2) ¬((¬P (b) → ¬S(a, b)) → T (a))^3.^¬→

(3g) ¬P (b) → ¬S(a, b) (3d) ¬T (a) (4) P (a) → Q(a) (5) P (b) → Q(b) (6) ∃y (R(y) ∧ S(y, a))

(7) ∃y (R(y) ∧ S(y, b)) (8) (R(a) ∧ Q(a)) → T (a)

(9) (R(b) ∧ Q(b)) → T (b)

(10) ∀y ((T (a) ∧ S(y, a)) → T (a))^12.^?^{a 13.}^?^b (11) ∀y ((T (y) ∧ S(y, b)) → T (b))^14.^?^{a 15.}^?^b

(12) (T (a) ∧ S(a, a)) → T (a) (13) (T (a) ∧ S(b, a)) → T (a) (14) (T (y) ∧ S(a, b)) → T (b) (15) (T (y) ∧ S(b, b)) → T (b)

.. .

Wykonali´smy wszystkie kroki dotycz ˛ace γ-formuł oraz stałych a i b. Jest wi- doczne, ˙ze druga formuła zmusza do wprowadzania coraz to nowych stałych (tak, jak ma to miejsce w formułach (6) oraz (7) powy˙zej). W konsekwencji, nie mo˙zna zako´nczy´c budowy tablicy analitycznej w tym przypadku.

6. Lawina miło´sci. Jak si˛e wydaje (przyjmuj ˛ac, ˙ze pasywizacja w j˛ezyku natu- ralnym odpowiada braniu konwersu relacji), strukturze składniowej zdania O ile cho´cby jeden osobnik jest zakochany sam w sobie, to je´sli ka˙zdy kogo´s kocha, to kto´s jest kochany przez wszystkichodpowiada nast˛epuj ˛ace zdanie j˛ezyka KRP:

(F) ∃x xK(x, x) → (∀x∃y K(x, y) → ∃y∀x K(x, y))

(13)

Spróbujemy zbudowa´c tablice analityczne: dla zdania (F) oraz dla jego zaprzeczenia. Najpierw tablica dla (F):

∃x K(x, x) → (∀x∃y K(x, y) → ∃y∀x K(x, y)) ^1.^→

H HH HH H HH HH H

(1_l) ¬∃x K(x, x) ^2.^?^a (2) ¬K(a, a)

◦

(1p) ∀x∃y K(x, y) → ∃y∀x K(x, y) ^3.^→

H HH HH H H

(3l) ¬∀x∃y K(x, y) ^4.

√

a

(4) ¬∃y K(a, y) ^5.^?^a (5) ¬K(a, a)

◦

(3p) ∃y∀x K(x, y) ^6.

√

a

(6) ∀x K(x, a) ^7.^?^a (7) K(a, a)

◦ Zauwa˙zmy, ˙ze w lewej gał˛ezi tablicy nie mieli´smy do dyspozycji δ-formuły, pozwalaj ˛acej wprowadzi´c now ˛a stał ˛a. W takiej sytuacji wprowadzamy now ˛a stał ˛a na mocy reguły dla γ-formuł. Otrzymana tablica nie jest zamkni˛eta, a wi˛ec jej gał˛ezie otwarte (akurat wszystkie s ˛a otwarte) s ˛a spełnialne.

Zauwa˙zmy równie˙z, ˙ze mo˙zemy wprowadza´c t˛e sam ˛a stał ˛a dla δ-formuł, znaj- duj ˛acych si˛e na ró˙znych gał˛eziach (mo˙zna te˙z zawsze u˙zywa´c ró˙znych stałych na poszczególnych gał˛eziach).

Teraz spróbujemy zbudowa´c tablic˛e analityczn ˛a dla negacji zdania (F):

(14)

¬(∃x K(x, x) → (∀x∃y K(x, y) → ∃y∀x K(x, y))) ^1.^¬→

(1_g) ∃x K(x, x) ^3.

√

a1

(1d) ¬(∀x∃y K(x, y) → ∃y∀x K(x, y)) ^2.^¬→

(2_g) ∀x∃y K(x, y) ^4.^?â¹ ^8.^?â² ^10.^?â³ (2d) ¬∃y∀x K(x, y) ^5.^?â¹^9.^?â² ^11.^?â³

(3) K(a1, a1) (4) ∃y K(a1, y) ^6.

√

a2

(5) ¬∀x K(x, a1) ^7.

√

a₃

(6) K(a1, a2) (7) ¬K(a₃, a₁) (8) ∃y K(a₂, y) ^12.

√

a₄

(9) ¬∀x K(x, a₂) ^13.

√

a5

(10) ∃y K(a3, y) ^14.

√

a6

(11) ¬∀x K(x, a3) ^15.

√

a7

...

Nie mo˙zna zakończyć budowy tej tablicy. W ten oto sposób jeden samolub uruchomił pot˛e˙zn ˛a (nieskończon ˛a!) lawin˛e miło´sci. Czy potrafisz napisać wzór na miło´sćukryty w tej konstrukcji? Mówi ˛ac powa˙znie: czy potrafisz wskazać model, w którym prawdziwa byłaby negacja zdania (F)?

Jerzy Pogonowski Zakład Logiki i Kognitywistyki UAM www.kognitywistyka.amu.edu.pl http://logic.amu.edu.pl/index.php/Dydaktyka pogon@amu.edu.pl

(15)

Wybrane pozycje bibliograficzne

Annelis, I.A. 1990. From Semantic Tableaux to Smullyan Trees: A History of the Development of the Falsifiability Tree Method. Modern Logic 1, 36–69.

Bell, J.L., Machover, M. 1977. A Course in Mathematical Logic. North-Holland Publishing Company, Amsterdam New York Oxford.

Beth, E.W. 1955. Semantic Entailment and Formal Derivability. Mededelingen der Koninklijke Nederlandse Akademie van wetenschapen, afd. letterkunde, new series, vol. 18, no. 13, Amsterdam.

Fitting, M. 1990. First-Order Logic and Automated Theorem Proving. Springer Verlag, New York Berlin Heidelberg London Paris Tokyo Hong Kong.

Gentzen, G. 1935. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift39, 176–210, 405–431.

Georgacarakos, G.N., Smith, R. 1979. Elementary Formal Logic. McGraw-Hill Book Company.

Handbook of Automated Reasoning.2001. A. Robinson, A. Voronkov (eds.), El- sevier, Amsterdam London New York Oxford Paris Shannon Tokyo, The MIT Press, Cambridge, Massachusetts.

Handbook of Tableau Methods. 1999. Edited by: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J., Kluwer Academic Publishers, Dordrecht Boston London.

Hintikka, J. 1955. Form and Content in Quantification Theory. Acta Philosophica Fennica8, 7–55.

Hodges, W. 1977. Logic. Pelican Books.

Howson, C. 1997. Logic with trees. Routledge, London and New York.

Jeffrey, R. 1991. Formal Logic: Its Scope and Limits. McGraw-Hill, New York.

Kleene, S.C. 1967. Mathematical Logic. John Wiley & Sons, Inc. New York Lon- don Sydney.

Kripke, S. 1959. A Completeness Theorem in Modal Logic. Journal of Symbolic Logic24, 1–14.

(16)

Lis, Z. 1960. Wynikanie semantyczne a wynikanie formalne. Studia Logica X, 39–60.

Marciszewski, W., Murawski, R. 1995. Mechanization of Reasoning in a Histori- cal Perspective.Rodopi, Amsterdam – Atlanta.

Nerode, A., Shore, R.A. 1997. Logic for Applications. Graduate Texts in Compu- ter Science, Springer.

Pawlak, Z. 1965. Automatyczne dowodzenie twierdze´n. Pa´nstwowe Zakłady Wy- dawnictw Szkolnych, Warszawa (seria: Biblioteczka Matematyczna, 19).

Por˛ebska, M., Sucho´n, W. 1991. Elementarne wprowadzenie w logik˛e formaln ˛a.

Pa´nstwowe Wydawnictwo Naukowe, Warszawa.

Priest, G. 2001. An Introduction to Non-Classical Logic. Cambridge University Press.

Quine, W.V. 1955. A proof procedure for quantification theory. The Journal of Symbolic LogicVolume 20, Number 2, 191–149.

Rasiowa, H., Sikorski, R. 1960. On the Gentzen Theorem. Fundamenta Mathe- maticae48, 58–69.

Rasiowa, H., Sikorski, R. 1963. The Mathematics of Metamathematics. Pa´nstwowe Wydawnictwo Naukowe, Warszawa.

Smullyan, R. 1968. First-Order Logic. Springer Verlag, Berlin.

Schütte, K. 1956. Ein System des verknüpfenden Schliessens. Archiv für mathematische Logik und Grundlagenforschungen2, 56–67.

Wang, H. 1960. Toward Mechanical Mathematics. IBM Journal Research and Development4, 2–22.

M ETODY D OWODZENIA T WIERDZE ´N I A UTOMATYZACJA R OZUMOWA ´N