SUPORT EXAMEN PROGRAMARE LOGICĂ

1. Programare Logică - cazul logicii Horn

Logica de ordinul I (calculul cu predicate).
• Un limbaj L de ordinul I este format dintr-o mulţime numărabilă de variabile V = {xn | n ∈ N}, conectorii ¬, →, ∧, ∨, paranteze, cuantifica-
torul universal ∀ şi cuantificatorul existenţial ∃, o mulţime P de simboluri de relaţii, o mulţime F de simboluri de funcţii, o mulţime C de
simboluri de constante, o funcţie aritate ar : F ∪ P → N∗ .
• Termenii lui L sunt definiţi inductiv asftel: orice variabilă este un termen; orice simbol de constantă este un termen; dacă f ∈ F, ar(f ) = n
şi t1 , . . . , tn sunt termeni, atunci f (t1 , . . . , tn ) este termen. Mulţimea termenilor lui L este notată cu T rmL .
• Dacă R ∈ R, ar(R) = n şi t1 , . . . , tn sunt termeni, atunci R(t1 , . . . , tn ) este formulă atomică.
• Formulele lui L sunt definite asftel: orice formulă atomică este o formulă; dacă A este o formulă, atunci ¬A este o formulă; dacă A şi B sunt
formule, atunci A ∨ B, A ∧ B, A → B sunt formule; dacă A este o formulă şi xi este o variabilă, atunci (∀xi )A, (∃xi )A sunt formule.
• O structură este de forma S = (S, FS , PS , CS ), unde S este o mulţime nevidă, FS = {f S | f ∈ F} este o mulţime de operaţii pe A (dacă
f are aritatea n, atunci f S : S m → S), RS = {RS | R ∈ R} este o mulţime de relaţii pe A (dacă R are aritatea n, atunci RS ⊆ S m ), şi
CS = {cS ∈ S | c ∈ C}.
• O interpretare a variabilelor lui L ı̂n S este o funcţie I : V → S. Interpretarea termenului t ı̂n S sub I (tS I ) este definită inductiv prin:
– dacă t = xi ∈ V , atunci tS I := I(xi )
– dacă t = c ∈ C, atunci tS I := c
S

– dacă t = f (t1 , . . . , tn ), atunci tS S S S

I := f ((t1 )I , . . . , (tn )I )
• O formulă este adevărată ı̂n S sub interpretarea I dacă:
– |= P (t1 , . . . , tn ) dacă P S (tS
S, I S
1 , . . . , tn )
– S, I
|= ¬B dacă S, I 6|= B
– S, I
|= B ∨ C dacă S, I |= B sau S, I |= C
– S, I
|= B ∧ C dacă S, I |= B si S, I |= C
– S, I
|= B → C dacă S, I 6|= B sau S, I |= C
– S, I
|= (∀x)B dacă pentru orice interpretare Ix←a avem S, Ixi ←a |= B
– S, I
|= (∃x)B dacă există o interpretare
( Ix←a astfel ı̂ncât S, Ixi ←a |= B
I(y) dacă y 6= x
unde pentru orice a ∈ S, Ix←a (y) =
a dacă y = x
• O formulă A este adevărată ı̂ntr-o structură S, notat S |= A, dacă este adevărată ı̂n S sub orice interpretare. Spunem că S este model al lui
A. O formulă A este adevărată ı̂n logica de ordinul I, notat |= A, dacă este adevărată ı̂n orice structură.
• O formulă G este o consecinţă logică a formulelor F1 , . . . , Fn , notat F1 , . . . , Fn |= G, dacă pentru orice structură S, dacă S |= Fi , i = 1, . . . , n,
atunci S |= G.
• Logica clauzelor definite/Logica Horn – un fragment al logicii de ordinul I ı̂n care singurele formule admise sunt clauze definite:
– formule atomice: P (t1 , . . . , tn )
– A1 ∧ . . . ∧ An → B, unde toate Ai , B sunt formule atomice.
• Problema programării logice: T |= A1 ∧ . . . ∧ An , unde T mulţime de clauze definite şi toate Ai sunt formule atomice.

Algoritmul de unificare.
• O subtituţie σ este o funcţie (parţială) de la variabile la termeni, adică σ : V → T rmL .
• Doi termeni t1 şi t2 se unifică dacă există o substituţie θ astfel ı̂ncât θ(t1 ) = θ(t2 ).
• Un unificator ν pentru U este un cel mai general unificator (cgu) dacă pentru orice alt unificator ν 0 pentru U , există o substituţie µ astfel
ı̂ncât ν 0 = ν; µ, unde ν; µ este compunerea substitutiilor ν şi µ.
Lista soluţie Lista de rezolvat
S R
· ·
Iniţial ∅ t1 = t01 , . . . , tn = t0n
0 ·
SCOATE S R,t=t
S R0
·
DESCOMPUNE S R , f (t1 , . . . , tn ) = f (t01 , . . . , t0n )
0
· 0 ·
S R , t1 = t1 , . . . tn = t0n
0
0 · ·
REZOLVĂ S R , x = t sau t = x, x nu apare ı̂n t
·
x = t, S[x ← t] R0 [x ← t]
Final S ∅

Rezoluţie SLD.
• O clauză definită P1 ∧ . . . ∧ Pn → Q poate fi gândită ca formula Q ∨ ¬P1 ∨ . . . ∨ ¬Pn .
• Pentru o mulţime de clauze definite T , regula rezolutiei SLD este
¬P1 ∨ · · · ∨ ¬Pi ∨ · · · ∨ ¬Pn
SLD
(¬P1 ∨ · · · ∨ ¬Q1 ∨ · · · ∨ ¬Qm ∨ · · · ∨ ¬Pn )θ
unde Q ∨ ¬Q1 ∨ · · · ∨ ¬Qm este o clauză definită din T (ı̂n care toate variabilele au fost redenumite) şi θ este c.g.u pentru Pi şi Q.
• Fie T o mulţime de clauze definite şi P1 ∧ . . . ∧ Pm o ţintă, unde Pi sunt formule atomice. O derivare din T prin rezoluţie SLD este o secvenţă
G0 := ¬P1 ∨ . . . ∨ ¬Pm , G1 , . . ., Gk , . . . ı̂n care Gi+1 se obţine din Gi prin regula SLD. Dacă există un k cu Gk =  (clauza vidă), atunci
derivarea se numeşte SLD-respingere.
Teoremă 1 (Completitudinea SLD-rezoluţiei). Sunt echivalente:
(1) există o SLD-respingere a lui P1 ∧ . . . ∧ Pm din T ,
(2) T |= P1 ∧ · · · ∧ Pm .

• Fie T o mulţime de clauze definite şi o ţintă G0 = ¬P1 ∨ . . . ∨ ¬Pm . Un arbore SLD este definit astfel:
– Fiecare nod al arborelui este o ţintă (posibil vidă)
– Rădăcina este G0
– Dacă arborele are un nod Gi , iar Gi+1 se obţine din Gi folosind regula SLD folosind o clauză Ci ∈ T , atunci nodul Gi are copilul Gi+1 .
Muchia dintre Gi şi Gi+1 este etichetată cu Ci .
• Dacă un arbore SLD cu rădăcina G0 are o frunză  (clauza vidă), atunci există o SLD-respingere a lui G0 din T .

2. Algebre multisortate
Signaturi multisortate. Mulţimi şi funcţii multisortate.
• O signatură multisortată este o pereche (S, Σ), unde S 6= ∅ este o mulţime de sorturi şi Σ este o mulţime de simboluri de operaţii σ :
s1 s2 . . . sn → s. Dacă n = 0, atunci σ :→ s este simbolul unei constante.
Fixăm o mulţime de sorturi S.
• O mulţime S-sortată este o familie de mulţimi A = {As }s∈S .
• O funcţie S-sortată f : A → B este o familie de funcţii f = {fs }s∈S , unde fs : As → Bs , pt. or. s ∈ S. Dacă f : A → B şi g : B → C,
definim compunerea f ; g : A → C, (f ; g)s (a) = gs (fs (a)), or. a ∈ As .
• O funcţie S-sortată f : A → B este injectivă, (surjectivă, bijectivă) dacă fs este injectivă, (surjectivă, bijectivă), or. s ∈ S. O funcţie
S-sortată f = {fs }s∈S : A → B este inversabilă dacă există g : B → A astfel ı̂ncât f ; g = 1A şi g; f = 1B .

Propoziţie 1. O funcţie S-sortată f : A → B este inversabilă ⇔ este bijectivă.

Algebre multisortate.
• O algebră multisortată de tip (S, Σ) este A = (AS , AΣ ) unde AS = {As }s∈S este o mulţime S-sortată şi AΣ = {Aσ }σ∈Σ este o familie de
operaţii astfel ı̂ncât
– dacă σ : s1 . . . sn → s ı̂n Σ, atunci Aσ : As1 × . . . × Asn → As .
– dacă σ : → s ı̂n Σ, atunci Aσ ∈ As .

Morfisme de algebre multisortate.

• Un morfism de (S, Σ)-algebre h : A → B este o funcţie S-sortată h = {hs }s∈S : {As }s∈S → {Bs }s∈S care verifică condiţia de compatibilitate:
– hs (Aσ ) = Bσ , or. σ :→ s ∈ Σ,
– hs (Aσ (a1 , . . . , an )) = Bσ (hs1 (a1 ), . . . , hsn (an )), or. σ : s1 . . . sn → s ∈ Σ şi or. a1 ∈ As1 , . . . , an ∈ Asn .

Propoziţie 2. Compunerea a două Σ-morfisme este un Σ-morfism.

Izomorfisme de algebre multisortate.

• Un Σ-morfism h : A → B se numeşte izomorfism dacă există un Σ-morfism g : B → A astfel ı̂ncât h; g = 1A şi g; h = 1B . Deoarece g este
unic, se notează cu h−1 .
• Două Σ-algebre A şi B sunt izomorfe (A ' B) dacă există un izomorfism f : A → B.

Propoziţie 3. Fie h : A → B un Σ-morfism. Atunci h este izomorfism ⇔ este funcţie S-sortată bijectivă.

Propoziţie 4. Compunerea a două izomorfisme f : A → B şi g : B → C este un izomorfism. Mai mult, (f ; g)−1 = g −1 ; f −1 .

Tipuri abstracte de date.

• Un tip abstract de date este o clasă C de (S, Σ)-algebre cu proprietatea că oricare două (S, Σ)-algebre din C sunt izomorfe.
• I(S,Σ) = {I | I (S, Σ)-algebră iniţială} este un tip abstract de date.

Termeni. Algebre de termeni.

• O mulţime de variabile este o mulţime S-sortată X = {Xs }s∈S astfel ı̂ncât Xs ∩ Xs0 = ∅, or. s, s0 ∈ S, s 6= s0 , Xs ∩ {σ}σ:s1 ...sn →s∈Σ = ∅ şi
Xs ∩ {σ}σ:→s∈Σ = ∅.
S
• Mulţimea S-sortată a termenilor cu variabile din X, TΣ (X), este cea mai mică mulţime de şiruri finite peste alfabetul L = s∈S Xs ∪
S
w,s Σw,s ∪ {(, )} ∪ {, } care verifică:
– X ⊆ TΣ (X),
– dacă σ :→ s ı̂n Σ, atunci σ ∈ TΣ (X)s ,
– dacă σ : s1 . . . sn → s ı̂n Σ şi ti ∈ TΣ (X)si , or. 1 ≤ i ≤ n, atunci σ(t1 , . . . , tn ) ∈ TΣ (X)s .
• Mulţimea S-sortată a termenilor TΣ (X) este o (S, Σ)-algebră, numită algebra termenilor cu variabile din X, cu operaţiile definite astfel:
pt. or. σ :→ s din Σ, operaţia corespunzătoare este Tσ := σ ∈ TΣ (X)s şi pt. or. σ : s1 . . . sn → s din Σ, operaţia corespunzătoare este
Tσ : TΣ (X)s1 ...sn → TΣ (X)s , Tσ (t1 , . . . , tn ) := σ(t1 , . . . , tn ), or. t1 ∈ TΣ (X)s1 , . . . , tn ∈ TΣ (X)sn . TΣ algebra termenilor fără variabile
(X = ∅).
• O substituţie a variabilelor din X cu termeni din TΣ (Y ) este o funcţie S-sortată τ : X → TΣ (Y ).
2
Ecuaţii. Relaţia de satisfacere.
·
• O (S, Σ)-ecuaţie (∀X)t =s t0 este formată dintr-o mulţime de variabile X şi doi termeni t, t0 ∈ TΣ (X)s .
·
• O (S, Σ)-algebră A = (AS , AΣ ) satisface o ecuaţie (∀X)t =s t0
– dacă pentru orice funcţie S-sortată e : X → AS , ẽs (t) = ẽs (t0 ).
– dacă pentru orice morfism f : TΣ (X) → A, fs (t) = fs (t0 ).
·
• O (S, Σ)-ecuaţie condiţionată (∀X)t =s t0 if H este formată dintr-o mulţime de variabile X, doi termeni de acelaşi sort t, t0 ∈ TΣ (X)s şi o
·
mulţime H de ecuaţii u =s0 v, cu u, v ∈ TΣ (X)s0 .
·
• O (S, Σ)-algebră A = (AS , AΣ ) satisface o ecuaţie condiţionată (∀X)t =s t0 if H
·
– dacă pentru orice funcţie S-sortată e : X → AS , ẽs0 (u) = ẽs0 (v), or. u =s0 v ∈ H ⇒ ẽs (t) = ẽs (t0 ).
·
– dacă pentru orice morfism f : TΣ (X) → A, fs0 (u) = fs0 (v), or. u =s0 v ∈ H ⇒ fs (t) = fs (t0 ).

3. Logica ecuaţională

Deducţie ecuaţională.
• E mulţime de ecuaţii necondiţionate
· · ·
(∀X)t1 =s t2 (∀X)t1 =s t2 , (∀X)t2 =s t3
R · S ·
T ·
(∀X)t =s t (∀X)t2 =s t1 (∀X)t1 =s t3

· ·
(∀X)t1 =s1 t01 , . . . , (∀X)tn =sn t0n
CΣ ·
, unde σ : s1 . . . sn → s ∈ Σ
(∀X)σ(t1 , . . . , tn ) =s σ(t01 , . . . , t0n )

·
SubE · , (∀Y )t =s t0 ∈ E şi θ : Y → TΣ (X)
(∀X)θ(t) =s θ(t0 )
·
• Ecuaţia  := (∀X)t =s t0 se deduce din E dacă ex. o secvenţă 1 , . . . , n a.ı̂. n =  şi pt. or. 1 ≤ i ≤ n:
– i ∈ E sau
– i se obţine din 1 , . . . , i−1 aplicând una din reg. R, S, T, CΣ, SubE .

Corectitudinea si completitudine logicii ecuaţionale.

1 , . . . , n
• O regulă de deducţie este corectă dacă Γ |= 1 , . . . , Γ |= n ⇒ Γ |= .


Propoziţie 5. Regulile de deducţie R, S, T, CΣ, SubΓ sunt corecte.

· ·
Teoremă 2 (Corectitudinea deducţiei). Γ ` (∀X)t =s t0 ⇒ Γ |= (∀X)t =s t0 .
· ·
Teoremă 3 (Completitudinea deducţiei). Γ |= (∀X)t =s t0 ⇒ Γ ` (∀X)t =s t0 .

4. Rescrierea termenilor
Contexte.
• nry (t) = numărul de apariţii ale lui y ı̂n t
• Fie z a.ı̂. z ∈
/ X. Un termen c ∈ TΣ (X ∪ {z}) se numeşte context dacă nrz (c) = 1. 
t0 , dacă x = z
• Dacă t0 ∈ TΣ (X) şi t0 are acelaşi sort cu z, definim substituţia {z ← t0 } : X ∪ {z} → TΣ (X), prin {z ← t0 }(x) = .
x, altfel
Pentru un context c ∈ TΣ (X ∪ {z}), notăm c[z ← t0 ] := {z ← t0 }(c).

Sistem de rescriere.
• O regulă de rescriere l →s r (peste Y ) este formată din l, r ∈ TΣ (Y )s astfel ı̂ncât l nu este variabilă şi V ar(r) ⊆ V ar(l).
• Un sistem de rescriere (TRS) este o mulţime finită de reguli de rescriere.
• Dacă R este un sistem de rescriere, pentru t, t0 ∈ TΣ (X)s definim relaţia t →R t0 astfel:

t →R t0 ⇔ t este c[z ← θs (l)] şi

t0 este c[z ← θs (r)], unde
c ∈ TΣ (X ∪ {z}) context,
l →s r ∈ R cu V ar(l) = Y ,
θ : Y → TΣ (X) substituţie

·
• Dacă E este o mulţime de ecuaţii astfel ı̂ncât, pt. or. (∀Y )l =s r ∈ E, l ∈
/ Y (nu este variabilă) şi V ar(r) ⊆ V ar(l), definim sistemul de
·
rescriere determinat de E RE := {l →s r | (∀Y )l =s r ∈ E}. Notăm relaţia de rescriere generată de RE prin →E := →RE .
· ∗
Teoremă 4. E ` (∀X)t =s t0 ⇔ t ↔E t0 .
3
Sisteme de rescriere abstracte.
• Un sistem de rescriere abstract este o pereche (T, →) unde T este o mulţime şi →⊆ T × T .
• t ∈ T este reductibil dacă există t0 ∈ T a.ı̂. t → t0 .
• t ∈ T este ı̂n formă normală (ireductibil) dacă nu este reductibil.
∗
• t0 este o formă normală a lui t dacă t → t0 şi t0 este ı̂n formă normală.
∗ ∗
• t1 şi t2 se intâlnesc (t1 ↓ t2 ) dacă există t ∈ T a.ı̂. t1 → t ← t2 .
• (T, →) se numeşte
– noetherian: dacă nu există reduceri infinite t0 → t1 → t2 → . . ..
∗ ∗
– confluent: t1 ← t → t2 ⇒ t1 ↓ t2 .
– local confluent: t1 ← t → t2 ⇒ t1 ↓ t2 .
∗
– Church-Rosser: t1 ↔ t2 ⇒ t1 ↓ t2 .
– normalizat: orice element are o formă normală.
– complet (convergent, canonic): confluent şi noetherian.
∗
Propoziţie 6. Fie (T, →) sistem de rescriere. Dacă t ↓ t0 , atunci t ↔ t0 .
Propoziţie 7. Dacă (T, →) este un sistem de rescriere noetherian, atunci orice element are o formă normală.
Propoziţie 8. Dacă (T, →) este un sistem de rescriere complet, atunci orice element are o unică formă normală.
Propoziţie 9. Un sistem de rescriere este confluent ddacă este Church-Rosser.
Propoziţie 10. Dacă (T, →) este un sistem de rescriere confluent, atunci este local confluent.
Propoziţie 11. Dacă (T, →) este un sistem de rescriere noetherian şi local confluent, atunci este confluent.
∗
Propoziţie 12. Fie (T, →) sistem de rescriere complet. Atunci t ↔ t0 ⇔ f n(t) = f n(t0 ).
· ∗
Corolar 1. Dacă sistemul de rescriere (TΣ (X), RE ) este complet, atunci E ` (∀X)t =s t0 ⇔ t ↔E t0 ⇔ fn(t) = fn(t’).