Logica per la programmazione - Appunti

Logica per la programmazione

Indice

1. Regole di inferenza .......................................... pag. 1
2. Logica del primo ordine .................................... pag. 3
3. Leggi su quantificatori non standard ............... pag. 6
4. Sintassi dei predicati ....................................... pag. 8
5. Triple di Hoare ................................................ pag. 10

Regole di inferenza

1.1 Commutatività
p ∨ q ≡ q ∨ p
p ∧ q ≡ q ∧ p

1.2 Associatività
p ∨ (q ∨ r) ≡ (p ∨ q) ∨ r
p ∧ (q ∧ r) ≡ (p ∧ q) ∧ r

1.3 Idempotenza
p ∨ p ≡ p
p ∧ p ≡ p

1.4 Uniti
p ∧ ⊤ ≡ p
p ∨ ⊥ ≡ p

1.5 Zero
p ∧ ⊥ ≡ ⊥
p ∨ ⊤ ≡ ⊤

1.6 Distributività
p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)

1.7 Assorbimento
p ∧ (p ∨ q) ≡ p
p ∨ (p ∧ q) ≡ p

1.8 Doppia negazione
¬(¬p) ≡ p

1.9 Terzo escluso
p ∨ ¬p ≡ ⊤

1.10 Contraddizione
p ∧ ¬p ≡ ⊥

1.11 De Morgan
¬(p ∨ q) ≡ ¬p ∧ ¬q
¬(p ∧ q) ≡ ¬p ∨ ¬q

1.12 Tautologia
p ≡ ⊤

1.13 Completo
p ∨ (¬p ∧ q) ≡ p ∨ q
p ∧ (¬p ∨ q) ≡ p ∧ q

1.14 Eliminazione ≡
(p ⇒ q) ≡ ¬p ∨ q

1.15 Eliminazione ≡≡
(p ≡ q) ≡ (p ⇒ q) ∧ (q ⇒ p)

1.16 Modus Ponens
(p ∧ (p ⇒ q)) ⇒ q

1.17 Semp. ⇒
p ∧ q ⇒ p

1.18 Riduzione ad assurdo
(p ⇒ q) ⇒ ¬p

1.19 Contraposizione
(p ⇒ q) ≡ (¬q ⇒ ¬p)

1.20 Scambio
p ∧ q ⇒ c ≡ p ∨ ¬r ⇒ ¬q

1.21 Transitività ⇒
((p ⇒ q) ∧ (q ⇒ r)) ⇒ (p ⇒ r)

1.22 Eliminazione ≡≡ bis
(p ≡ q) ≡ (p ∧ q) ∨ (¬p ∧ ¬q)

1.23 Taut. ∨
p ≡ p ∨ q

1.24 Tollendo Ponens
(p ∨ q) ∧ ¬p ⇒ q

1.25 Tollendo Tollens
((p ⇒ q) ∧ ¬q) ⇒ ¬p

1.26 Sempl. Destra
(p ⇒ q) ∧ (q ⇒ r) ⇒ (p ⇒ q ∧ r)
(p ⇒ q) ∨ (q ⇒ r) ⇒ (p ⇒ q ∨ r)

1.27 Sempl. Sinistra
(p ⇒ q) ∨ (q ⇒ r) ⇒ (p ∧ q) ⇒ r
(p ⇒ q) ∧ (q ⇒ r) ⇒ (p ∨ q) ⇒ r

1.28 Sempl. Sinistra
(p ⇒ q) ∧ (q ⇒ r) ⇒ (p ∧ q) ⇒ r

1.31 Sempl.
(p ⇒ q) ∧ ((r ⇒ s) ⇒ (p ∧ r) ⇒ s) ⇔ (p ⇒ q) ∧ (p ∧ r ⇒ s ⇒ p ∧ s)

1.30 Risoluzione
(p ∨ q) ∧ (p ⇒ q ∨ r) ⇔ (q ∨ r)

1.32 Silogismo disgiuntivo
(p ∨ q) ∧ ((p ⇒ r) ∧ (q ⇒ s)) ⇔ (r ∨ s)

1.33 Assurdo
(p ⇒ ⊥) ⇔ ¬p

1.33 Diversione
((q ⇒ p) ∧ (q ⇒ s? p)) ⇔ p

1.34 E: Uni ⇒ V
(∀x, P) ⇔ P(x)

1.35 Intro: ∃
P(x) ∧ x ⇔ ∃x, p

1.36 De Morgan
¬(x ∈ P) ⇔ ∀x, ¬P
¬(∀x, p) ⇔ ∃x, ¬p

1.37 Annidamento
(∀x, ∀y, P) ⇔ ∀y, (∀x, P))
(∃x, (∃y, p)) ⇔ (∃y, (∃x, P))

1.38 ∀∀ A e ∃∀ V
(∀x, P(x, P) ⇔ (∀x, ∀x, Q) ⇔ (∃x, P ∨ Q) ⇔ (∀x, x, Q ∨ x)

1.39 Costante
(∀x, P) ⇔ P (x ∴ P) ⇔ Px

1.40 ∃ R e ∀: V
(∃x P ∧ R) ⇔ (x ∶ P) ∧ (∃x, Q)(x ∶ P) ∨ (∀x Q) ⇔ (∀x, P ∨ Q)

1.41 Leibniz
x = y ⇔ (p = p (p x, y)(x = y ∧ p)⇔(x = y ∧ p(x)(x ≠ y ∧ P) ⇔ P(y)

1.42 Singoletto
(∀x x ≠ ∃x, x) ⇔ ((∃x, x ≠ A P) ⇔ P) ⇔

1.43 Generalizzazione
(∀P(x))[(P(x) con q nuovo costante)

1.44 I;: formalizzazione
(∀P(P(x) con q nuovo costante)

1.45 Intervallo
(x ∈ [a, b]): ∧ (∀x, x K, Q) ∧ ∧ ∀xi x ∈ [a, l) x x K, Q) a, b) (x ≠ c) _y a, b) x[(∀x, x ∈ [a, b]): ∧ (∀x, x Q)) ∀ K, Q) Q(∃x, ∈ [a, l) x x a) ∧ ∀

1.46 Dominio
(∀x, P ∨ Q) > = R) ⇔ (∀x, P ⇒ R) ∧ (∀x, Q ⇒ R)(∃x, P ∨ Q) ∧ R) ⇔ (∃x ∧ P ∧ R) ∨ (∃x ∧ Q ∧ R)

Logica del primo ordine

Sintassi

Perché una frase sia corretta occorre che sia ben definita la sua sintassi, cioè il suo linguaggio. Il linguaggio (L) è basato su di un alfabeto.

Alfabeto

L'alfabeto di un linguaggio è composto da:

• Costanti (c)
• Funzioni (F)
• Variabili (V)
• Predicati (P)
• Connettivi logici (¬, ∧, ∨, ⇒, =)
• Quantificatori (∀, ∃)
• Parentesi ({}, {}, {}, {})

Termini

I termini di un linguaggio sono sequenze di simboli appartenenti al dominio o soggetti dei predicati. C e Y sono due possibili termini con possibili specifici elementi degli insiemi E e F.

Formule

Le formule sono degli aspetti connessi con gli elementi del linguaggio degli assiomi nel linguaggio usiamo. E.g. (∀x ((P ∧ R) ∨ (Q ∨ P) ⇒ (∀z . S))) è una formula.

Semantica

La semantica di una formula stabilisce il suo valore di verità. Nei casi di formule chiuse (non con variabili quantificati) è definita la verità (la verità è determinata con regole di interpretazione che definiscono il significato dei simboli che compongono.

Interpretazioni

Le interpretazioni devono stabilire:

• Domini
• Elementi di c
• Elementi di V
• Elementi di P
• Definizione del significato dei vari simboli

Assegnare: D = insieme domini E = {costanti} F = {schede} P = {predicati} f (costi, constar) = elemento di valore costante I = (D, α₂) A_V (costante) = elemento di valore costante A (macrodeclarcy) (χ) = J, se φ, in valore affermato

Assegnazione

Un assegnamento è una funzione φ che assegna le convocato del dominio a una variabile Esempio: e¹_a(Y) = 5 |θ se x=x|θ (Y) 0 cercare Se la variabile ν assume valore k dei laboratoristi se φ battersde cose restituita variabile Esempio:

Semantica dei connettivi

¬φ = ¬PI_α (φ) = I_α (P) dove ♯ = F in e per o ♯) φ = P Λ QI_α (φ) = ♯, se I_α (P)=♯, se I_α(Q)=♯, affermati φ = P V QI_α (φ) = ♯, se I_α (P) = ♯ I_α (Q) = ♯ altrimenti φ = P ⇒ QI_α (φ) = se I_α (P)=♯ e I_α (Q)=♯, I_α(P) = ♯ altrimenti φ = P ⇔ QI_α (φ) = ♯, se I_α (P) = ♯, se I_α (Q) = ♯, eppure se I_♤ (P) = ♯ e I_α (φ) = ♯. Affermati

Semantica dei quantificatori

φ = (χ_Α, β)I_α (φ) = ♯, se I_α (c1)[χ(P)] = ♯ per qualunque χ D, l^{♤ (φ)=♯ affermati} φ = (∃χ₁, P)I_α1 (φ) = ♯, se c'è elemento x₁ D per cui I_α[χ(P)]= ♯

Dimostrazioni

Per sostituzione per ≡

(Q ≡ R) ⊆ Γ ⊢ P ≡ P

Sostituzione per ≡ ⇒

(Q ≡ R) ⊆ Q occorre positivamente in P Γ ⊢ P ≡ P

Teorema di deduzione ⇒

Γ ⊢ P → Q ≡ Γ, P ⊢ Q

Leggi su quantificatori non standard

3.1 min_u ⇒ (∀_x.P ⇒ Q) ⇒ (min_x.P.E) > (min_x.Q.E)

3.2 max ⇒ (∀_x.P ⇒ Q) ⇒ (max_x.P.E) ≤ (max_x.Q.E)

3.3 m u == (∀_x.P ≡ Q) = (m_x.P.E) = (u_x.Q.E)

3.4 # ⇒ (∀_x.P ≡ Q) ⇒ (# _x:P(R) = (# _x:Q(R)

3.5 # ⇒ (∀_x.P ⇒ Q) ⇒ (#_x:P(R) < (#_x:Q(R))(∀_x.R ≥ S) ⇒ (#_x:P(R) ⋐ (∀_x:P(S))

3.6 Σ == (∀_x.P ≡ Q) ⇒ (Σ_x:P.E) ≡ (Σ_x:Q.E)

3.7 Σ = ⇒ (∀_x.E ≥ 0 ∧ P ⇒ Q) ⇒ (Σ_x:P.E) ≤ (Σ_x:Q.E)(∀_x.E < 0 ∧ P ≡ Q) ⇒ (Σ_x:P.E) ≥ (Σ_x:Q.E)

3.8 Σ Π + (Σ_x:P(E + F) = (Σ_x:P.E) + (Σ_x:P.F)

3.9 con:, max, min(con x.P v Q.E) = (con_x.P.E) max (con x.P.F)(min x.P v Q.E) = (min_x.P.E) min (min x.P.F)

3.10 dominio (Σ x : P v Q.R.E) = (Σ x . P.E) + (Σ x . Q.T) - (Σx PΛ Q.T)#_x:P v Q(R = )#_x:P(R) + (#_x:Q.R) - #_x:P Λ Q.R)(u_x:P v Q.E) = (u_x:P.E) u (u_x.Q.E)

3.11 costante (Σ_x:P.C) = c * (Σ_x.P.T) se x non è libero in c se x non è libero in c ∧ P ≠ ∅

3.12 Distributivo {Σ x: P . d + E} = d (Σ x: P . E) se x una variabile libera in c (u x: P . c + E) = c (u x: P . E) se x una variabile libera in c e P =/= ∅

3.13 Singoletto {Σ x: x = y,E} = E_y# {x: x = y|R}_y = 1 se R^y0 se -R^y(u x: x = y,E) = E^y

3.14 Vuoto {Σ x: P . E} = 0# x . P (x) = 0(u x: P . E) = +∞(u x: P . E) = +∞ se P = ∅

3.15 Intervallo {Σ x: x ∈ (a,b) ∧ x /∈ K ( . P . E) + E^k se p^k{x: x ∈ (a,b) ∧ x ∉ K ∧ P . E} se p^k# {x ∈ (a,b) |P}_s = # {x ∈ (a,b)/ x /∉ K ∧ P}_t# (w x: x ∈ [a,b] ∧ x /∉ K ∧ P . E) = u^ex se p^k(w x: x ∈ (a,b) ∧ x /∉ K ∧ P . E) u^e se p^k(u x x ∈ (a,b) ∧ x ∉ K . E) se p^k

3.16 # ≡ ∀# {x ∈ (a,b)}| P = 0 ≡ {x ∉ (a,b) . ¬P}# 3.12 = 3 ## {x ∈ (a,b)|P] > 0 ≡ {x ∈ (a,b) . P}

3.18 massivo e unio V(∀ x ∈ (a,b). ¬P) ≡ (formalite (max x ∈ (a,b)|P) = -∞ (∀ x ∈ (a,b)).¬P) ≡ (min x ∈ (a,b)) | P) = +∞

3.28 supx : 1= P _∃ ∃x ∈ (a,b) . P) ⇒ (supx x ∈ (a,b) (P) ∈ (a,b) ∃x ∈ (a,b) . P) ⇒ (u = (supx x ∈ (a,b)) (P) ≡ u ∈ [a,b] ∧ P (u) ∧ (∀y ∈ (a,u) ¬P(y)) ∀x ∈ (a,b) ) ∅) ⇒ ( sup x ∈ (a,b) (P) ∈ (a,b)∃x ∈(a,b).P) ⇒ (u = (supx x∈(a,b) (p) ≡u ∈ (a,b)¬P (u) ∧ (∀y∈(a,u)¬P(y))

Sintassi dei predicati

Fbf → Prop | Fbf ∧ FbfProp → Impl | Prop ≡ PropImpl → Giunz | Giunz ⇒ ImplGiunz → Aud | OrAud → Audprium | AudpriumOr → Orprium | OrpriumAudprium → Pium (Or)Orprium → Pium (Aud)Pium → Atom ∧ AtomAtom → ⌝ | ⌥ | Ide (Prop) | Pred (Term = Term | Fbf)QuumIde → p | qFbf Quum → (∃ Var . Fbf) (∀ Var . Fbf)Pred → P Ide (Term {, Term})Term → Const | Var | F Ide (Term | Term)(∑ Var . Fbf . Term) ⌈#⌊ ∀ Var . Fbf ⌋ Fbf⌉ (⌈wx Var : Fbf . Term⌉) ⌈ ∑wx Var : Fbf . Term⌉ Exp⌉Exp → , , * , / operazioni aritmeticheConst → 0 | 1 | 2 | ... | +00 | -00 | ...

Triple di Hoare

Le triple di Hoare sono un metodo per specificare le proprietà di programmi e poter verificare il corretto funzionamento. {P} C {R} Nella tripla scritta sopra abbiamo: due asserzioni che descrivono le caratteristiche che il programma deve soddisfare nello stato iniziale; un comando che una volta verificata la prima asserzione, modifica lo stato del programma in uno che, dopo l'esecuzione del comando, dovrà soddisfare la seconda asserzione.

Asserzioni

Le asserzioni descrivono insiemi di stati ed il loro linguaggio è un'estensione del linguaggio delle espressioni booleani. (x-y) Le asserzioni possono confluire variabili e quantificatori; nell'asserzione con essi possono essere parti posticipate per quantificare e esse possono descrivere variabili dette libere se non compaiono nella quantificazione e perciò legate legate. Le variabili legate invece sono quelle che compaiono nella quantificazione e per questo legate. In particolare un'asserzione si definisce chiusa se la lista di variabile legata è vuota.

Lettura delle triple

Le triple di Hoare possono essere lette in tre modi: {P} C {R} Sicuramente: E ogni stato p e c e proviamo R in un modo che una volta eseguito il prog e soddisfatto. Specifica: L'esecuzione più stata p e r e dobbiamo determinare quale è il comando da eseguire per ottenere il risultato richiesto. Correttamente: Abbiamo tutta la tripla e dobbiamo verificare la correttezza.

Pre + Post Condizione

La regola dei pre-post condizione è un sottocchio per verificare la coerenza delle asserzioni iniziale e quella finale. P ⇒ P'{P'} C {R'}R' ⇒ R{P} C {R} Significa: P ⇒ P' = P R = R'