Logică - Varianta 2

Subiectul a fost preluat de pe site-ul Info3BNecenzurat. Rezolvarea subiectului este originală.

1. a) Definiția constructivă a noțiunii de term in LP1.

Baza. X ⊆ T şi Fo ⊆ T (variabilele şi constantele sunt termi).

Pas constructiv. Pentru fiecare n ∈ N*, pentru fiecare f ∈ Fn, pentru fiecare t₁, t2, …, tn ∈ T, avem f(t₁, t₂, ……, t_n) ∈ T. Concluzionăm această etapă a definiţiei prin a „spune” că At ⊆ LP1.


b) Să se găsescă o structură S care să fie model pentru: F = (∀z)(P(f(z), g(z))) ∧ Q(a, b).

Trebuie să găsim o structură de forma: S = <U_S, I_S>.

Luăm U_S = N;

P^s: N² → B; p^s (x, y) = 1 dacă x < y

Q^s: N² → B; q^s (x, y) = 1 daca x = y

f^s: N → N; f^s (x) = x+1

g^s: N → N; g^s (x) = x+2

Se observă că pentru a, b = 1 și oricare ar fi z formula este adevărată tot timpul.
 

2. a) Teorema de substituție din LP1.

Fie H ∈ LP1, oarecare. Fie orice F, G ∈ LP1 astfel încît F este o subformulă a lui H şi G este tare echivalentă cu F. Fie H’ formula obţinută din H prin înlocuirea (unei apariţii fixate a) lui F cu G. atunci H este echivalent cu H’.
 

b) Aduceți următoarea formulă în FNSC: (∃x)(Q(x,y)) → (P(x) → ¬(∃x)(Q(y,x))).

Mai întâi aducem formula în formă cauzală:

F = (∃x)(Q(x,y)) → (¬P(x) ∨ (∃x)(Q(y,x))). ⇔

F = (∀x)¬(Q(x,y)) ∨ ¬P(x) ∨ (∃x)(Q(y,x)).

Acum trecem formula F în FNR utilizând substituția [x/z], [y/u] și [x/t] pentru clauza a doua și a treia.

F = (∀x)¬(Q(x,y)) ∨ ¬P(z) ∨ (∃t)(Q(y,t)).

Trecem formula în FNPR.

F = (∀x)(∃y)(∃z)(∃t)(¬(Q(x,y)) ∨ ¬P(z) ∨ Q(y,t)).

Aplicăm substituțiile următoare: [y/f(x)], [z/g(x)] și [t/h(x)] și formula noatră devine:

F = (∀x)(¬(Q(x,f(x))) ∨ ¬P(g(x)) ∨ Q(f(x),h(x))), formulă ce se afla în FNSC.


3. a) Definiția noțiunii de teoremă într-un sistem deductiv.

Fie SD = <A, R> un sistem deductiv în FORM. Mulţimea teoremelor lui SD este mulţimea metaformulelor care admit demonstraţii în SD, adică:

Th(SD) = {F ∈ FORM | există o demonstraţie D pentru F în SD }.


b) Demonstați, folosind rezoluția pură, că următoarea formulă este nesatisfiabilă:

F = (∀x)( ∀y)(P(x,x) ∧ (¬P(x,g(y)) ∨ Q(y)) ∧ ¬Q(f(a))).

Despărțim formula F în clauze și aplicăm algoritmul rezoluției și avem:

Am ajuns la clauza vidă deci formula F este nesatisfiabilă.