Backward chaining

Il backward chaining o backward reasoning (lett. risp. "incatenamento a ritroso" e "ragionamento a ritroso") è un metodo di ragionamento automatico che consiste, intuitivamente, nel ragionare partendo dall'obiettivo e procedere a ritroso verso i dati a disposizione. Viene usato per la dimostrazione automatica di teoremi, per il funzionamento dei motori inferenziali ed altre applicazioni nel campo dell'intelligenza artificiale. L'opposto del backward chaining è il forward chaining.^[1]

Nella teoria dei giochi, questo tipo di ragionamento viene chiamato induzione a ritroso e consiste nel cercare sottogiochi (più semplici) per trovare la soluzione del gioco di partenza. Negli scacchi, in particolare, è chiamato analisi retrograda.

In programmazione logica, il backward chaining è implementato mediante la risoluzione SLD.^[2]

Funzionamento

Il backward chaining inizia da una lista di obiettivi (o ipotesi) e ragiona "all'indietro", partendo dalle conseguenze delle regole di inferenza disponibili e verificando se le premesse sono (ricorsivamente) note essere vere. Se esiste un fatto o un insieme di fatti che rendono (ricorsivamente) vere le premesse, allora l'ipotesi di partenza è verificata.

Visto che sono gli obiettivi di partenza a determinare la scelta delle regole di inferenza, il metodo è definito "goal-driven", in contrasto con il metodo forward chaining che è definito "data-driven".

Esempio

Supponiamo che l'obbiettivo sia quello di trovare il colore di un certo animale di nome Fritz, sapendo che esso gracida e mangia le mosche e conoscendo le seguenti regole di inferenza:

1. Se X gracida e X mangia mosche, allora X è una rana.
2. Se X cinguetta e X canta, allora X è un canarino.
3. Se X è una rana, allora X è verde.
4. Se X è un canarino, allora X è giallo.

Assumiamo veri i seguenti fatti:

1. Fritz gracida
2. Fritz mangia le mosche

Ragionando tramite backward chaining, il motore inferenziale può derivare che Fritz è verde tramite la seguente serie di passaggi:

1. Dato che è possibile unificare l'obiettivo di partenza con la conseguenza della regola n° 3 (in particolare quando "Fritz è verde"), sostituiamo in quest'ultima X con Fritz, ottenendo una nuova ipotesi, ovvero:
   • Fritz è una rana
   che andiamo aggiungere alla "catena" di obiettivi da verificare.
2. Dato che l'obiettivo "Fritz è una rana" unifica con la conseguenza della regola n° 1, sostituiamo in quest'ultima X con Fritz, ottenendo due nuove ipotesi, ovvero:
   • Fritz gracida
   • Fritz mangia le mosche
   che andiamo aggiungere alla "catena" di obiettivi da verificare e che dovranno essere veri contemporaneamente (in quanto la premessa della regola n° 1 è una congiunzione logica).
3. Verifichiamo che gli obiettivi "Fritz gracida" e "Fritz mangia le mosche" sono veri, in quanto presenti tra i fatti conosciuti. Di conseguenza l'intera catena di obiettivi è soddisfatta per modus ponens e, in particolare, l'obiettivo di partenza risulta essere verificato.

Da notare che:

• in generale, non tutte le regole di inferenza sono necessarie per verificare l'ipotesi;
• l'obiettivo lo si fa corrispondere sempre ad una conseguenza affermativa (e non negativa, come nel modus tollens);
• le premesse non vengono implicate dalle conseguenze (altrimenti si ricadrebbe nella fallacia dell'affermazione del conseguente), ma diventano a loro volta nuovi obiettivi da verificare.

Implementazione

Il Backward Chaining generalmente è implementabile come una Pila:

1. Viene aggiunto in cima allo stack il fatto di cui si vuole verificare la consequenzialità logica;
2. Viene rimossa la formula presente sulla cima dello stack, e viene fatto il push delle formule presenti nella Knowledge Base che sono antecedenti di un'implicazione avente come conseguente la formula estratta.

La procedura termina quando:

1. Lo stack risulta vuoto: in questo caso si ha una terminazione con successo. Verrà restituito il valore True, corrispondente al fatto che la formula da verificare sia effettivamente conseguenza logica della Knowledge Base.
2. Lo stack non viene svuotato, pur applicando tutte le formule presenti nella Knowledge Base. In questo caso, si deduce che la formula da verificare non è conseguenza logica della KB, dunque non è derivabile da essa.