[AI][Logica Proposizionale] inferenza, deduzione ed implicazione logica
Salve a tutti, sono alle prese con questo tipo di logica e mentre studio sul celeberrimo R&N, ho alcuni punti che non mi tornano o su cui ho fatto confusione.
Parliamo di Agenti basati su logiche, hanno una loro KB all'interno composta da fatti e assumptions. Tramite deduzione possiamo ricavare/derivare nuove sentences che andranno a popolare la KB dell'agente diventando anche esse dei facts.
Il Libro però prima introduce il concetto di ENTAILMENT, in cui una sentence alpha è entailed da una KB se in ogni interpretazinoe in cui KB è vera anche alpha lo è. Si parla quindi di model checking, ovvero di cercare tra tutti i modelli possibili tramite tabella di verità le righe in cui la nostra KB è true e verificare che anche alpha sia true in quelle interpeteazioni.
Poi si passa al concetto di deduzione, che ha un altro simbolo e a quanto ho capito si basa sull'applicazione delle regole di inferenza come Modus Ponens, And elimination etc.
Ad esempio Forward Chaining and Backward chaining sono due algoritmi che fanno inferenza derivando nuove sentences usando solo Modus Ponens (almeno FC). Però è un algoritmo completo, cioè ogni sentence derivata con FC è anche entailed logicamente nella KB che si usa in partenza.
Quello che non capisco è, l'entailment logico e la deduzione logica, sono entrambi processi che generano nuove sentences ma si basano su idee diverse?
Parliamo di Agenti basati su logiche, hanno una loro KB all'interno composta da fatti e assumptions. Tramite deduzione possiamo ricavare/derivare nuove sentences che andranno a popolare la KB dell'agente diventando anche esse dei facts.
Il Libro però prima introduce il concetto di ENTAILMENT, in cui una sentence alpha è entailed da una KB se in ogni interpretazinoe in cui KB è vera anche alpha lo è. Si parla quindi di model checking, ovvero di cercare tra tutti i modelli possibili tramite tabella di verità le righe in cui la nostra KB è true e verificare che anche alpha sia true in quelle interpeteazioni.
Poi si passa al concetto di deduzione, che ha un altro simbolo e a quanto ho capito si basa sull'applicazione delle regole di inferenza come Modus Ponens, And elimination etc.
Ad esempio Forward Chaining and Backward chaining sono due algoritmi che fanno inferenza derivando nuove sentences usando solo Modus Ponens (almeno FC). Però è un algoritmo completo, cioè ogni sentence derivata con FC è anche entailed logicamente nella KB che si usa in partenza.
Quello che non capisco è, l'entailment logico e la deduzione logica, sono entrambi processi che generano nuove sentences ma si basano su idee diverse?
Risposte
Ma perché scrivi mezzo in inglese mezzo in italiano...?
Mi sembra comunque che il succo della tua domanda sia:
Qual è la differenza tra dire "l'enunciato A è conseguenza logica di B, ovvero B è vera in ogni modello in cui A è vera" e " B è dimostrabile a partire da A tramite gli assiomi e le regole di inferenza" . Il primo è un concetto semantico, il secondo è sintattico e dipende dal sistema formale in cui fai le dimostrazioni. La scelta delle regole di inferenza dovrebbe essere tale da garantire un teorema di validità (che dice che ogni volta che B è dimostrabile a partire da A, B è conseguenza logica di A) e auspicabilmente un teorema di completezza ( che dice che ogni cosa che è conseguenza logica degli assiomi della teoria è dimostrabile)
Mi sembra comunque che il succo della tua domanda sia:
Qual è la differenza tra dire "l'enunciato A è conseguenza logica di B, ovvero B è vera in ogni modello in cui A è vera" e " B è dimostrabile a partire da A tramite gli assiomi e le regole di inferenza" . Il primo è un concetto semantico, il secondo è sintattico e dipende dal sistema formale in cui fai le dimostrazioni. La scelta delle regole di inferenza dovrebbe essere tale da garantire un teorema di validità (che dice che ogni volta che B è dimostrabile a partire da A, B è conseguenza logica di A) e auspicabilmente un teorema di completezza ( che dice che ogni cosa che è conseguenza logica degli assiomi della teoria è dimostrabile)
Quindi l'inferenza è il processo che si applica per fare Deduzione logica e Ragionamento Logico (che sono sinonimi)? Purtroppo ho usato tante fonti e ognuno chiama le cose in modo diverso.
Ad esempio, sia in PL che in FOL, sia modus ponens che resolution sono due tecniche di inferenza giusto? Come mai resolution l'ho sempre vista associata ad un metodo di deduzione logica mentre modus ponens no?
Grazie
Ad esempio, sia in PL che in FOL, sia modus ponens che resolution sono due tecniche di inferenza giusto? Come mai resolution l'ho sempre vista associata ad un metodo di deduzione logica mentre modus ponens no?
Grazie
Il consiglio generale che ti do e' di ignorare il modo in cui ognuno chiama i vari concetti perché tra filosofia , matematica e informatica credo che ognuno usi un po' i termini che vuole per dire più o meno le solite cose.
Ti faccio un riassunto un po' approssimativo per farti un'idea:
in generale un calcolo logico è un sistema formale che ti permette di fare dimostrazioni, ed è il dato di un insieme di assiomi logici (cioè un particolare insieme possibilmente infinito di tautologie da cui parti per fare dimostrazioni) e un insieme (possibilimente infinito) di regole di inferenza che utilizzi per derivare teoremi partendo dagli assiomi. Prima di tutto bisogna scegliere il tipo di logica, che può essere usando le tue sigle FOL o PL, e ovviamente classica o non classica. La scelta degli assiomi da utilizzare e delle regole di inferenza varia tantissimo a seconda di cosa vuoi fare con questo calcolo. Puoi ridurre al minimo cioè all'insieme vuoto gli assiomi e avere solo regole di inferenza, o tenere ad esempio come regola solo il modus ponens e avere più assiomi. A seconda dell'utilizzo che vuoi fare di questo calcolo logico sceglierai regole e assiomi che ti garantiscano dei metateoremi che ti fanno comodo: ad esempio il teorema di completezza, oppure ad esempio puoi aver bisogno che il calcolo sia refutazionalmente completo. In generale una regola di inferenza, per essere valida , deve essere tale che ogni volta che le premesse sono tutte vere , è vera anche la conseguenza.
Ti faccio un riassunto un po' approssimativo per farti un'idea:
in generale un calcolo logico è un sistema formale che ti permette di fare dimostrazioni, ed è il dato di un insieme di assiomi logici (cioè un particolare insieme possibilmente infinito di tautologie da cui parti per fare dimostrazioni) e un insieme (possibilimente infinito) di regole di inferenza che utilizzi per derivare teoremi partendo dagli assiomi. Prima di tutto bisogna scegliere il tipo di logica, che può essere usando le tue sigle FOL o PL, e ovviamente classica o non classica. La scelta degli assiomi da utilizzare e delle regole di inferenza varia tantissimo a seconda di cosa vuoi fare con questo calcolo. Puoi ridurre al minimo cioè all'insieme vuoto gli assiomi e avere solo regole di inferenza, o tenere ad esempio come regola solo il modus ponens e avere più assiomi. A seconda dell'utilizzo che vuoi fare di questo calcolo logico sceglierai regole e assiomi che ti garantiscano dei metateoremi che ti fanno comodo: ad esempio il teorema di completezza, oppure ad esempio puoi aver bisogno che il calcolo sia refutazionalmente completo. In generale una regola di inferenza, per essere valida , deve essere tale che ogni volta che le premesse sono tutte vere , è vera anche la conseguenza.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo