Logica per l'informatica

Premessa

Ciao! Se è la prima volta che capiti su questo sito, ti consiglio di consultare la pagina principale di questo cosiddetto Giardino Digitale per scoprire meglio cos’è e come navigarlo.

Lo stato di questa nota è al momento: 🔴 Bozza.

---

Logica PER l’informatica: perché PER?

Focus: sintassi e semantica (interpretazione semantica della sintassi)
Fare differenza tra matematici “puri” e “sporchi”

1 - Strumenti

Rocq = proof assistant (prima si chiamava Coq, cambiato nome per un motivo)

• funzionale
• si cerca dimostrazioni da formule

Z3 = SMT-solver = dimostra teoremi

• si dimostra che formule sono soddisfacibili

2 - Esempio

Abbiamo due affermazioni:

1. “Se $x$ è un numero primo maggiore di $2$, allora $x$ è dispari” che si rappresenta in simboli come:

$$\text{prime}(x)\wedge x>2⟹\text{odd}(x)$$

2. “Non esiste un caso in cui $x$ non è un numero primo maggiore di $2$”:

$$\overline{\overline{\text{prime}(x)\wedge x>2}}$$

Domanda: è vero che $x$ non è dispari? In simboli:

$$\overline{\text{odd}(x)}$$

Come facciamo a rispondere a questa domanda?

Procedimento:

1. Astraiamo dal significato vero e proprio delle proposizioni
2. Concentriamoci sulla struttura logica delle proposizioni:
   1. Introduciamo variabili proposizionali:

$$\begin{array}{c}A:=\text{prime}(x)\wedge x>2\\ B:=\text{odd}(x)\end{array}$$

2. Riformuliamo il problema: "Possono le tre proposizioni logiche $A \implies B$, $\overline{\overline A}$ e $\overline B$ reggere?"
	Cioè:
	$$
	A \implies B \land \overline{\overline A} \land \overline B \overset{?}{=} TRUE
	$$

2.1 - Soluzione model-teorica/combinatoria

Esaminiamo tutte le possibili combinazioni:

[Tabella]

Non c’è un valore di verità che soddisfa tutte le formule proposizionali in una sola volta, quindi:

• il problema non ha un modello
• il problema è insoddisfacibile

2.2 - Soluzione deduttiva/proof-theoretic

$$\frac{\overline{B}}{}$$

Questa derivazione ha:

• Delle assunzioni di partenza:
• Delle regole:
• Una conclusione: falso

Quindi \notB non può essere compatibile con \not\notA e $A⟹B$.

3 - Esempio 2

---

Fonti

• 🏫 Corso di Laurea in Informatica (L-31 R) presso l’Università di Torino:
  • Corso di Logica per l’Informatica, A.A. 2025-26 (pagina Moodle):
    • Prof. Roversi Luca, slide del corso:
      • Organizzazione
      • Preludio
    • Prof. Roversi Luca, videoregistrazioni del corso:
      • Organizzazione
      • Preludio 1
      • Preludio 2
      • Preludio 3