Istanziazione universale
L'istanziazione universale è una regola di sostituzione di una variabile x in una formula f(x) con un termine ground ossia con un valore ( informazione ). Nella logica del primo ordine l'istanziazione universale consente di trasformare una formula logica caratterizzata dalla presenza di un quantificatore universale con l'insieme di tutte le possibili istanze.
Ad esempio, in una base di conoscenza della logica del primo grado è presente una formula in cui si afferma che "tutte le persone respirano quando sono vive". La formula è caratterizzata dal quantificatore universale "per ogni" ( ∀ ). La regola di istanziazione universale consente di trasformare l'inferenza del primo ordine in un problema di inferenza proposizionale.
Il processo di istanziazione universale analizza gli oggetti (x) della base di conoscenza (KB) che rispondono alla proprietà Persona() e si associa la proprietà Respira() a tutti quelli che non sono morti ( ¬Morto(x) ) creando tre distinte istanze. La regola trasforma la formula della logica del primo ordine ( ∀x ) in un insieme di istanze di logica proposizionale. L'istanziazione universale è una delle principali tecniche di proposizionalizzazione.
Logiche equivalenti. Le due rappresentazioni sono logicamente equivalenti. In entrambi i casi la base di conoscenza può rispondere alla domanda "Giuseppe respira?". La logica del primo ordine associa una proprietà all'insieme di oggetti che rispondono a una particolare caratteristica. La logica proposizionale, invece, associa la proprietà a ogni singolo oggetto che risponde a una particolare caratteristica.
Annidamento infinito dei termini. L'annidamento è uno dei problemi della proposizionalizzazione tramite l'instanziazione universale. Ad esempio, se la base di conoscenza contiene al suo interno la formula Madre(x), la proposizionalizzazione crea un'istanza Madre(x) per ogni valore della variabile x ma anche un'istanza Madre(Madre(x)) per indicare la nonna di x, un'istanza Madre(Madre(Madre(x))), e così via sempre più in profondità all'infinito. Questo fenomeno causa un annidamento infinito dei termini.
- Terminazione in profondità ( taglio ). Per evitare l'annidamento infinito in profondità si può imporre una terminazione a un determinato livello di profondità. Ciò consente di evitare i loop infiniti. La terminazione genera però un problema di incompletezza asimmetrica dell'analisi. Ad esempio, un algoritmo dimostra una conseguenza logica soltanto se riesce a verificare la formula prima della terminazione in profondità. Viceversa, l'algoritmo non può dimostrare l'assenza di una conseguenza logica quando non verifica la formula prima della terminazione, poiché nessuno può sapere con certezza se la soluzione si trovi più in profondità oppure no.
