La logica e lo studio del ragionamento corretto, in particolare di come si traggono inferenze.
La logica nasce come strumento per chiarire il ragionamento umano. Con Aristotele e poi con la logica matematica moderna diventa un modo per formalizzare proposizioni, regole e dimostrazioni. Boole, Frege, Russell, Hilbert e Godel sono tappe fondamentali di questo percorso.
Definizione
La logica computazionale e l’uso della logica in informatica: per computare, rappresentare computazioni e ragionare sulle computazioni.
In pratica: la logica puo servire a descrivere cosa deve valere in un sistema, dimostrare che un programma soddisfa una proprieta, oppure eseguire un programma come ricerca di una prova.
Note
Per Intelligent Systems Engineering, la logica e importante perche collega conoscenza, ragionamento, verifica e programmazione dichiarativa.
Verita, Sintassi e Semantica
Definizione
La sintassi riguarda la manipolazione dei simboli, mentre la semantica riguarda il significato dei simboli rispetto a un dominio di interpretazione.
Una frase puo essere vera per il suo significato oppure per la sua forma logica. “Socrate e uomo” e “tutti gli uomini sono mortali” implicano “Socrate e mortale” in base al significato dei predicati. Invece p e p -> q implicano q indipendentemente da cosa significhino p e q.
Definizione
Una conclusione e conseguenza logica di alcune premesse se e vera in ogni interpretazione in cui le premesse sono vere.
Tarski formalizza il legame tra simboli e dominio del discorso. Da qui nasce la doppia faccia della verita logica:
Proof theory: assiomi e regole di inferenza, lato sintattico.
Model theory: interpretazioni e verita, lato semantico.
Esempio: se ho p e p -> q, allora q segue sempre. Non importa se p significa “piove” o “il server e acceso”.
Computazione vs Deduzione
Definizione
La computazione parte da un’espressione e applica regole fisse per ottenere un risultato; la deduzione parte da una congettura e cerca una prova usando assiomi e regole di inferenza.
Computare sembra meccanico: eseguo passi determinati. Deducere puo richiedere scelta, creativita e ricerca. Il teorema di Fermat e un esempio estremo: la congettura era semplice da enunciare, ma dimostrarla ha richiesto secoli.
Eppure computazione e deduzione si incontrano:
Una computazione puo essere vista come dimostrazione di un teorema, ad esempio 15 + 26 = 41.
Una deduzione puo diventare computazione se fissiamo una strategia di proof search.
Punto Critico
Quando fissiamo una strategia, rimuoviamo il “guesswork”. Ma se non esiste una strategia automatica efficiente, torna lo spazio per scelta, conoscenza di dominio e autonomia.
Questo punto prepara il legame con agenti e AI: ragionare automaticamente significa esplorare spazi di prova, ma scegliere bene dove cercare richiede conoscenza e controllo.
Proof Search
Definizione
La proof search e la ricerca di una catena di inferenze che dimostri un giudizio o una congettura.
Una deduzione ha premesse, conclusione e regola di inferenza. Organizzando tutte le possibili catene di inferenza otteniamo un proof tree: la radice e la conclusione da provare, le foglie sono assiomi o giudizi gia noti.
Due strategie principali:
Forward chaining: parto dagli assiomi, genero nuovi teoremi e spero di raggiungere la congettura.
Backward chaining: parto dalla congettura, cerco quali premesse la dimostrerebbero e ricorro sui sotto-goal.
Esempio pratico: se voglio provare grandparent(lino, luca), in backward chaining cerco una regola che concluda grandparent(X,Z), poi devo provare parent(X,Y) e parent(Y,Z).
Sfide della Ricerca
Molte regole possono applicarsi insieme, alcuni rami possono divergere, gli alberi possono essere infiniti e la terminazione non e garantita.
Programmazione Logica
Definizione
La programmazione logica e un paradigma in cui programmi e conoscenza sono espressi come formule logiche, e l’esecuzione procede come dimostrazione di goal.
La svolta arriva con il principio di risoluzione di Robinson, l’unificazione e l’interpretazione procedurale delle clausole di Horn proposta da Kowalski. Prolog nasce nel 1973 trasformando un theorem prover in un linguaggio di programmazione.
Tre caratteristiche fondamentali:
Termini: dominio universale su cui si computa.
Most general unifier (mgu): sostituzione piu generale che rende compatibili due termini.
Backtracking: meccanismo di controllo per esplorare alternative.
Definizione
Un termine e una variabile, una costante, oppure un functor applicato ad altri termini.
Esempio: a, X, g(X,Y) e f(a, X, g(Y,b)) sono termini. Il termine strutturato puo essere visto come un albero.
Clausole, Goal e SLD Resolution
Definizione
Una clausola di Horn e una clausola logica con al massimo un letterale positivo; e la forma base dei programmi logici.
In un logic program:
Una rule ha forma A <- B1, ..., Bm.
Un fact e una regola senza corpo, cioe A <-.
Un goal e cio che vogliamo provare, ad esempio <- G.
La stessa clausola ha due letture:
Dichiarativa: A e vero se B1, ..., Bm sono veri.
Procedurale: per provare A, prova B1, ..., Bm.
Definizione
La SLD resolution e la procedura di risoluzione usata nella programmazione logica per provare goal tramite backward chaining e unificazione.
Se il goal corrente G unifica con la testa A di una clausola, si applica l’mgu e si sostituisce il goal con i sotto-goal del corpo. Se la lista dei goal diventa vuota, la derivazione ha successo; se nessuna clausola applicabile esiste, fallisce; se continua per sempre, non termina.
La lettura dichiarativa dice: X e nonno/nonna di Z se esiste Y tale che X e genitore di Y e Y e genitore di Z.
La lettura procedurale dice: per rispondere a grandparent(lino, luca), prova prima parent(lino,Y) e poi parent(Y,luca). L’unificazione trova Y = joey, poi il secondo goal ha successo.
Risultati tipici:
grandparent(lino, luca) ha successo.
grandparent(lino, joey) fallisce.
grandparent(lino, X) produce X = luca e X = simone.
Note
La programmazione logica e potente per knowledge representation, interrogazione e prototipazione AI, ma controllo e terminazione restano aspetti delicati.
Prossimi Argomenti
Continueremo con:
M9 - Automated Reasoning - tecniche automatiche di dimostrazione, SAT, model checking e logiche non classiche.
M10 - Planning - pianificazione automatica per agenti intelligenti.