Witam ponownie.
Rachunek Gentzena stanowi pewną odnianę formalizacji rachunku kwantyfikatorów szczególnie przydatną do automatyzacji procesu dowodzenia twierdze? rachunku kwantyfikatorów.
Rachunek Gentzena wprowadza do rachunku kwantyfika-torów pojęcie sekwencji < S, T > , która jest uporządkowaną parą zbiorów formuł < S, T >, gdzie:
S = {s1, s2, . . . ,sn } i T = {t1, t2, . . . ,tm}.
Przez sekwencję < S, T > rozumiemy następującą impli-kację
s1 &s2 & . . . & sn > t1 v t2 v . . . v tm
Sekwencję < S, T > będziemy oznaczali w następujący sposób
s1, s2, . . . ,sn f t1, t2, . . . ,tm
Jeżeli zbiory S i T zawierają wspólny element, to sekwencja < S, T > jest twierdzeniem, a zatem zdaniem zawsze prawdziwym (tautologią)
Oki chodzi więc o to: mamy jakieś zdanie logiczne np. f~ (a v b) =(~a &~b) gdzie
f -znak sekwencji gentzena
~ -negacja
v -alternatywa
-implikacja
& -koniunkcja
= -równoważność
I teraz wg. reguł wnioskowania rachunku Gentzena które brzmią:
Dla negacji
A1: P,~a f Q P f a,Q
A2: P f ~a,Q P,a f Q
Dla koniunkcji
B1: P, a & b fQ P, a, b f Q
B2: P f a & b, Q P f a, Q i P f b, Q
Dla alternatywy
C1: P, a v b f Q P, a f Q i P, b f Q
C2: P fa v b, Q P f a, b, Q
Dla implikacji
D1: P, a >b f Q P,b f Q i P f a, Q
D2: P f a >b, P, a f b, Q
Dla równoważności
E1: P, a =b f Q P, a, b f Q i P f a, b, Q
E2: Pf a = b, Q P, a f b, Q i P, b f a, Q
musimy sprawdzić czy zdanie jest tautologią
np: f ~ (a v b) = (~a &~b)
|
E2
|________________
| |
~ (a v b) f (~a &~b) (~a &~b) f ~ (a v b)
| |
B2 B1
________________________| |
| | ~a,~b f ~(av b)
~(av b) f ~a ~(av b) f ~b |
| | A2
A1 A1 |
| | ~a,~b, a v b f
f a v b,~a f a v b, ~b |
| | A1
C2 C2 |
| | ~b, av b f a
f a, b, ~a f a, b, ~b |
| | A1
A2 A2 |
| | a v b fa, b
a f a, b b fa, b |
C1
__|
| |
a f a, b b f a,b
Chodzi o to że napisałem procedurę sprawdzającą czy wpisane zdanie jest poprawne gramatycznie czyli jest tyle nawiasów co potrzeba czy znaki występujące po sobie są dopuszczalne itp.
A teraz ma mi rozbijać moje zdanie na pomniejsze sprawdzać czy to tautologia
POzdr.