Inferenza del primo ordine

L'inferenza del primo ordine è l'insieme di tecniche computazionali che consentono di applicare l'inferenza logica sulle informazioni rappresentate nella logica del primo ordine.

• Proposizionalizzazione. La proposizionalizzazione consiste nella trasformazione delle informazioni dalla logica del primo ordine alla logica proposizionale. È una tecnica efficace ma fortemente inefficiente, sia dal punto di vista dello spazio di memoria necessario a registrare tutte le proposizioni logiche della logica proposizionale ( complessità spaziale ) e sia per il tempo di esecuzione dell'algoritmo ( complessità temporale ).
• Inferenza per sostituzione / unificazione. Il processo di inferenza per sostituzione / unificazione compara ( unisce ) la formula della query con quelle presenti nella base di conoscenza. In caso di esito positivo, l'algoritmo sostituisce la variabile della query con il termine trovato. Il processo di unificazione ha il vantaggio di operare direttamente nella logica del primo ordine, senza dover trasformare la conoscenza in proposizioni logiche. È quindi una tecnica di inferenza del primo ordine più efficiente rispetto alla proposizionalizzazione.
• Metodo della risoluzione. Il metodo della risoluzione è un processo di inferenza per verificare se un'ipotesi è una conseguenza logica di una premessa. L'ipotesi da dimostrare viene negata. La risoluzione verifica se l'ipotesi negata è soddisfacibile per assurdo. Se l'ipotesi negata non è soddisfacibile, allora l'ipotesi iniziale è una conseguenza logica della premessa. Il metodo della risoluzione è applicabile alla logica del primo ordine quando la base di conoscenza è rappresentata nella forma normale congiuntiva ( CNF ). La risoluzione dimostra che KB è conseguenza logica di A provando che KB ∧ A non è soddisfacibile ( clausola vuota ).
• Concatenazione in avanti del primo ordine. Il processo di inferenza si basa sull'applicazione della tecnica della concatenazione in avanti alle formule della logica del primo ordine. Il processo di inferenza continua fin quando è possibile aggiungere nuove formule alla base di conoscenza a partire dalle formule già esistenti.
• Concatenazione all'indietro del primo ordine. Il processo di inferenza utilizza la ricerca in profondità a concatenazione all'indietro in una base di conoscenza della logica del primo ordine. A partire da un'ipotesi iniziale, l'algoritmo ricostruisce e verifica a ritroso tutte le premesse che la rendono vera. L'ipotesi di partenza è vera se e soltanto tutte le premesse inferite sono soddisfacibili tramite la base di conoscenza.