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 9
5. Triple di Hoare _pag 10

Regole di Inferenzia

1.1 Commutatività

p ∨ q ≡ q ∨ p

p ∧ q ≡ q ∧ p

1.2 Associazioni

p ∨ (q ∨ r) ≡ (p ∨ q) ∨ r

p ∧ (q ∧ r) ≡ (p ∧ q) ∧ r

1.3 Idempotenza

p ∨ p ≡ p

p ∧ p ≡ p

1.4 Unità

p ∧ T ≡ p

p ∨ F ≡ p

1.5 Zero

p ∧ F ≡ F

p ∨ T ≡ T

1.6 Distributiva

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 ≡ T

1.10 Contraddizione

p ∧ ¬p ≡ F

1.11 De Morgan

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

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

1.12 Tautologia

T ≡ F

F ≡ T

1.13 Complemento

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

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

1.14 Elim ➔

(p ➔ q) ≡ ¬p ∨ q

1.15 Elim ⇔

(p ⇔ q) ≡ (p ➔ q) ∧ (q ➔ p)

1.16 Modus Ponens

(p ∧ (p ➔ q)) ⇒ q

1.17 Semp ➔1

p ∧ q ⇒ p

1.18 Riduzione ad assurdo

(p ➔ q) ∧ ¬q ≡ ¬p

1.19 Controposizione

(p ➔ q) ≡ (¬q ➔ ¬p)

1.20 Scambio

p ∨ p ≡ c = p ∧ ¬r ≡ ¬q

1.21 Ristr ➔ 1

((p ➔ q) ∧ (q ➔ r)) ≡ (p ➔ r)

1.22 Elim ⇔ bis

(p ⇔ q) ≡ (p ∧ q) ∨ (¬p ∧ ¬q)

1.23 Ist ⊃ V

p ⇒ p ∨ q

1.24 Tollendo Ponens

(p ∨ q) ∧ ¬p ⇒ q

1.25 Tollendo Tollens

((p ➔ q) ∧ ¬q) ⇒ ¬p

2.3.5 Conseguenza Logica e Modelli

Si dice modello un'interpretazione a partire dalla quale si può dimostrare una formula φ.

Γ ⊨ φ

o per un insieme di formule Γ

Γ ⊨ Γ

2. Si dice conseguenza logica di un insieme Φ di formule Γ, la formula φ se per ogni modello di Γ a partire dai risultati di insieme Γ φ è conseguenza logica di φ.

Γ ⊨ φ

2.3 Dimostrazioni

2.3.1 Sostituzione per ≡

1. (Q ≡ R) ⊨ Γ
2. ⊨ P_Q ≡ P_R

2.3.2 Sostituzione per ⇒

1. (Q ⇒ R) ∈ Γ ⊨ Q
2. ⊨ P_R

(Q ⇒ R) ∈ M

⊨ P_R

2.3.3 Teorema di Deduzione

• Γ ⊨ P ⇒ Q ≡ Γ, P ⊨ Q

5. TRIPLE DI HOARE

Le triple di Hoare sono un metodo per specificare le proprietà di programmi e poterne verificare il corretto funzionamento.

{P} C {R}

Nella triple 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, modificando lo stato di programma inizia, dopo l'esecuzione del comando, dover essere verificata dal seconda asserzione.

5.1 ASSERZIONI

Le asserzioni descrivono sistemi di stati di caso linguaggio e un'estensione dei linguaggi delle espressioni booleane.

(Fx: F) Le asserzioni possono contenere variabile e quantificazioni: nell'asserzione è possibile usare queste variabili dette LIBERE se non compaiono nella parte del programma, deve essere legate all'asserzioni (dette LEGATE).

5.2 LETTURA DELLE TRIPLE

Le triple di Hoare possono essere lette in tre modi:

1. Semantica: valutiamo P e C e verifichiamo R in un modo che P viene soddisfatta
2. Specificamente: troviamo gli stati s in P e dobbiamo determinare comando da eseguire per ottenere il risultato richiesto
3. Correttamente: abbiamo tutto la tripla e dobbiamo verificare la correttezza.

5.3 PRE + POST CONDIZIONE

La regola di pre post condizione è un'asserzione per verificare la coerenza della asserzione iniziale e quella finale.

P -> P'{P} C {R}R' -> R

{P'} C {R'}

Significa:

• P -> P' = P ≅ P'
• -R' -> R = R' ≅ R
• -{P'} C {R'} = da uno stato P con l'esecuzione di C si deriva a uno stato R' e date le due condizioni precedenti, la tripla {P} C {R} è soddisfatta.