vuoi
o PayPal
tutte le volte che vuoi
SSE
ℒ ℒ
3.4 Calcolo per risoluzione
DEF. UTILI PER LA CFN (forma normale congiuntiva):
1. LETTERALE: si dice letterale una lettera enunciativa negata o meno;
2. CLAUSOLA: si dice clausola una disgiunzione finita di letterali (NB: esiste anche la clausola vuota, ovvero con nessun letterale □);
3. FORMA IN CLAUSOLE: una f.b.f. si dice in forma a clausole se è scritta come congiunzione di clausole.
{} { }
∪ ∪ ∪
DEF. REGOLA DI RISOLUZIONE: siano e clausole e un letterale. Dalle clausole e si deriva per risoluzione la clausola . In simboli
1 2 1 2 1 2
NB: la risoluzione è un sistema formale con una sola regola d’inferenza.
Deduzione: è chiamata così l’iterazione della regola di risoluzione. Viene rappresentata da un albero orientato binario etichettato i cui nodi sono clausole.
Derivabilità: una derivazione per risoluzione di una clausola da un insieme di clausole è un albero cha ha per radice e per foglie (alcune) clausole di e in cui i
⊢ .
nodi intermedi sono ottenuti per risoluzione dai precedenti. Se una tale derivazione esiste si dice che è derivabile da e si scrive ℛ
{} {,
⊨ ∨ ⊢ }:
NB: il metodo di risoluzione è corretto ma in generale non è completo. Infatti si ha ma sicuramente non può essere ℛ
Tuttavia il metodo è corretto e completo per refutazione, ovvero vale il seguente teorema.
TH. di correttezza e completezza: sia un insieme di clausole
⊢ □
(correttezza) se allora è insoddisfacibile;
ℛ
⊢ □.
(completezza) se è insoddisfacibile allora ℛ
⊨ Φ ):
Metodo per stabilire se (dati una f.b.f. e un insieme di f.b.f. {¬Φ}
⊨ Φ ∪
1. dal corollario 2 del th. di deduzione semantica si ha che SSE è insoddisfacibile;
¬Φ;
2. si portano in clausole le f.b.f. di e {¬Φ}
□ ∪ ⊨ Φ.
3. si applica il metodo di risoluzione delle clausole così ottenute, se riusciamo ad ottenere allora è insoddisfacibile e dunque
Per sistemi grandi non è facile applicare il metodo di risoluzione, vengono quindi introdotte.
DEF. CLAUSOLE DI HORN: sono clausole che contengono al massimo un letterale positivo. Esse se positive sono dette fatto, se negative goal, se miste legge.
non tutte le f.b.f. possono essere scritte in forma a clausole di Horn;
□)
affinché un insieme di clausole di Horn sia insoddisfacibile (ovvero che da esse si possa dedurre deve contenere almeno un goal e un fatto.
4. Logica del primo ordine
Sintassi
ALFABETO: l’alfabeto della logica del primo ordine contiene: , , …;
1. Costanti: formano un insieme COST al più numerabile, sono rappresentate con le prime lettere dell’alfabeto minuscolo , , … ∈ ℕ;
2. Variabili: formano un insieme VAR al più numerabile, sono rappresentate con le ultime lettere dell’alfabeto minuscolo o con dove
, , … , ∈ ℕ;
3. Lettere funzionali: rappresentate con lettere intermedie dell’alfabeto minuscolo dotate di apice intero naturale o con dove
, , … , ∈ ℕ;
4. Lettere predicative: rappresentate con le prime lettere dell’alfabeto maiuscolo dotate di apice intero naturale o con dove
NB: l’apice che compare nelle lettere funzionali e predicative viene detto di arità. Può essere omesso se non crea ambiguità.
"¬", " ∧ ", " ∨ ", " ⟹ ", " ⟺ ";
5. Connettivi logici: gli stessi della logica proposizionale
"∀" "∃";
6. Quantificatori: il quantificatore universale ed il quantificatore esistenziale
"(" ")".
7. Parentesi: aperte e chiuse
DEF. TERMINE: un termine è una sequenza di simboli dei primi 3 tipi costruita tramite le seguenti regole ricorsive
se è costante o una variabile allora è un termine;
( )
, … , , … ,
se è una lettera funzionale di arità e sono termini allora anche è un termine.
1 1
( ),
, … , , … ,
DEF. FORMULE ATOMICHE: una formula atomica è una sequenza del tipo ove è una lettera predicativa di arità e sono termini.
1 1
Φ
DEF. FORMULA BEN FORMATA (f.b.f.): una f.b.f. è una sequenza di simboli che con generica formula atomica e f.b.f. la grammatica delle f.b.f. è:
()|(¬Φ)|(∀(Φ))|(∃(Φ))|(Φ
Φ ≔ ∧ Φ)|(Φ ∨ Φ)|(Φ ⟹ Φ)|(Φ ⟺ Φ)
Φ Φ (Φ)
Sottoformule: data la f.b.f. le sue sottoformule sono le formule usate per costruire attraverso il procedimento ricorsivo definito sopra. L’insieme delle
Φ
sottoformule di viene definito ricorsivamente nel seguente modo:
() {};
Φ = (Φ) =
se e è una formula atomica allora
(Ψ)) {Φ}
Φ = Ψ ∗ (Φ) = ∪ (Ψ);
(∗
se e è una f.b.f. e rappresenta il connettivo unario o un quantificatore allora
(Θ)) {Φ}
Φ = ∘ Ψ, Θ ∘ (Φ) = ∪ (Ψ) ∪ (Θ).
((Ψ)
se e sono f.b.f. e rappresenta un connettivo binario allora
Rappresentazione: come in logica proposizionale ad ogni f.b.f. può essere associato un albero di struttura. L’albero si può costruire applicando il seguente algoritmo
la radice è etichettata con il primo connettivo o quantificatore che è stato eliminato (detto operatore principale);
se un nodo rappresenta una formula atomica allora è una foglia etichettata con tale formula;
(Ψ))
Φ = Ψ ∗
(∗
se un nodo rappresenta una sottoformula del tipo e è una f.b.f. e rappresenta il connettivo unario o un quantificatore allora esso è
∗ Ψ.
etichettato con ed ha per successore un nodo che è la radice dell’albero di struttura di
(Θ))
∘ ∘ ∘
((Ψ)
se un nodo rappresenta una sottoformula del tipo con connettivo binario allora esso è etichettato con ed ha per successori due nodi che
Ψ Θ.
sono la radice degli alberi di struttura e
Compressione: possono essere eliminate tutte le parentesi meno quelle che servono per individuare il connettivo principale di ogni sottoformula. Ulteriori parentesi
possono essere eliminate fissando in modo arbitrario un ordine di priorità nell’applicazione degli operatori. Noi useremo questa convenzione:
"¬" " ∧ " " ∨ " " ⇒ " " ⇔ ";
e i quantificatori precedono che precede che precede che precede
i connettivi uguali si intendono associati a sinistra, i quantificatori contigui si intendono applicati nell’ordine in cui si trovano.
VARIABILI LIBERE E VINCOLATE Φ Φ
Campo d’azione del quantificatore: data la f.b.f. contentente almeno un quantificatore. Il raggio d’azione del quantificatore è la sottoformula di il cui albero di
struttura ha come radice tale quantificatore. .
Occorrenza libera: una occorrenza di una variabile è libera se non è nel campo di azione di quantificatori che quantifichino
Φ Φ Φ.
Variabile libera: una variabile che compare in una f.b.f. si dice libera in se ha qualche occorrenza libera in
() :
Insieme delle variabili libere in viene definito ricorsivamente nel seguente modo
Φ Φ
se è una formula atomica tutte le variabili di sono libere;
Φ ¬Ψ (Φ) = (Ψ);
se è una f.b.f. del tipo allora
Φ Ψ ∘ Θ ∘ (Φ) = (Ψ) ∪ (Θ);
se è una f.b.f. del tipo con operatore binario allora
{∀,
Φ Ψ ∈ ∃} (Φ) = (Ψ)\{}.
se è una f.b.f. del tipo con allora
.
Occorrenza vincolata: una occorrenza di una variabile è vincolata se è nel campo di azione di quantificatori che quantifichino
Φ Φ Φ.
Variabile vincolata: una variabile che compare in una f.b.f. si dice vincolata in se ha qualche occorrenza vincolata in
() :
Insieme delle variabili vincolate in viene definito ricorsivamente nel seguente modo
Φ (Φ) = ∅;
se è una formula atomica allora
Φ ¬Ψ (Φ) = (Ψ);
se è una f.b.f. del tipo allora
Φ Ψ ∘ Θ ∘ (Φ) = (Ψ) ∪ (Θ);
se è una f.b.f. del tipo con operatore binario allora
{∀,
Φ Ψ ∈ ∃} (Φ) = (Ψ) ∪ {}.
se è una f.b.f. del tipo con allora
Φ (Φ) (Φ)
NB: ovviamente, data una f.b.f. gli insiemi e non sono necessariamente disgiunti.
(Φ) = ∅.
DEF. f.b.f. chiusa/aperta: una f.b.f. si dice chiusa se Una f.b.f. non chiusa si dice aperta.
{ }
Φ (Φ) = , … , ∀ ∀ … ∀ Φ Φ.
DEF. chiusura universale: data la f.b.f. con la f.b.f. chiusa si chiama chiusura universale di
1 1 2
{ }
Φ (Φ) = , … , ∃ ∃ … ∃ Φ Φ.
DEF. chiusura esistenziale: data la f.b.f. con la f.b.f. chiusa si chiama chiusura esistenziale di
1 1 2
Φ Φ Φ
DEF. termine libero per una variabile: sia un termine e una f.b.f., si dice termine libero per una variabile in se nessuna occorrenza libera di in cade nel
.
campo d’azione di un quantificatore che quantifichi una variabile che compare in
Semantica
Per dare una semantica (un significato) alle f.b.f. di un linguaggio del primo ordine serve specificare un contesto ovvero una struttura interpretativa.
Una struttura interpretativa di un linguaggio del primo ordine permette di leggere le f.b.f. di tale linguaggio in linguaggio naturale.
〈, 〉 ,
DEF. STRUTTURA INTERPRETATIVA (struttura, interpretazione): una struttura è una coppia dove sono:
D, dominio: è un insieme;
I, funzione interpretativa: è formata da 3 funzioni:
o ;
associa ad ogni costante del linguaggio un elemento di
1
o ;
associa ad ogni del linguaggio u