title: Backward chaining
text: # 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.
  