# 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.
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.

## 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:
* Se X gracida e X mangia mosche, allora X è una rana.
* Se X cinguetta e X canta, allora X è un canarino.
* Se X è una rana, allora X è verde.
* Se X è un canarino, allora X è giallo.
Assumiamo veri i seguenti fatti:
* Fritz gracida
* Fritz mangia le mosche
Ragionando tramite backward chaining, il motore inferenziale può derivare che Fritz è verde tramite la seguente serie di passaggi:
* 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: che andiamo aggiungere alla "catena" di obiettivi da verificare.
** Fritz è una rana
* 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: 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).
** Fritz gracida
** Fritz mangia le mosche
* 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:
* Viene aggiunto in cima allo stack il fatto di cui si vuole verificare la consequenzialità logica;
* 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:
* 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.
* 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.