Algoritmo di risoluzione

L'algoritmo di risoluzione è un algoritmo utilizzato per dimostrare un teorema e per risolvere un problema tramite l'inferenza per risoluzione. Data una conseguenza logica ( A B ), l'algoritmo trasforma la logica proposizionale in un insieme di clausole ( A ∧ ¬B ) è , in formato CNF ( forma normale congiuntiva ), e verifica l'eventuale insoddisfacibilità seguendo il metodo della risoluzione ( regola della risoluzione ) sulle clausole. Ogni coppia di clausole con letterali complementari viene confrontata per produrre una nuova clausola da aggiungere all'insieme ( fattorizzazione ).

  • Se durante il processo emerge come risultato una clausola vuota, ciò significa che l'insieme di clausole è insoddisfacibile. La clausola vuota implica che la disgiunzione è falsa, poiché una disgiunzione è vera soltanto se almeno uno dei letterali disgiunti è vero. È quindi una contraddizione. Se l'insieme di clausole ( A ∧ ¬B ) è insoddisfacibile, allora la conseguenza logica ( A B ) è vera.
  • Se il processo di fattorizzazione continua fino a concludere tutte le combinazioni di confronto tra le clausole, senza trovare una clausola vuota, allora l'insieme è soddisfacibile e la conseguenza logica ( A B ) è falsa.

L'algoritmo di risoluzione utilizza la tecnica logica della dimostrazione per assurdo. L'algoritmo di risoluzione è utilizzato nei sistemi esperti e nei software di ragionamento automatico ( intelligenza artificiale ) per attuare processi di inferenza logica su una base di conoscenza.

https://www.okpedia.it/algoritmo_di_risoluzione



note


  • Completezza dell'algoritmo. L'algoritmo di risoluzione è completo poiché, dato un insieme X di clausole, analizza tutte le coppie di clausole fino al momento in cui non è possibile produrre una nuova clausola da aggiungere all'insieme X ( insieme soddisfacibile ) o fino al momento in cui individua una clausola vuota ( insieme insoddisfacibile ).


Questo sito utilizza cookie tecnici. Sono presenti alcuni cookie di terzi ( Gooogle, Facebook ) per la personalizzazione degli annunci pubblicitari. Cliccando su OK, scorrendo la pagina o proseguendo la navigazione in altra maniera acconsenti all’uso dei cookie.

Per ulteriori informazioni o per revocare il consenso fai riferimento alla Privacy del sito.