Înlănțuire înapoi
Înlănțuirea înapoi sau raționamentul înapoi ( lit. resp. „Înlănțuirea înapoi” și „raționamentul înapoi”) este o metodă de raționare automată care intuitiv constă în raționamentul pornind de la obiectiv și procedând înapoi către datele disponibile. Este utilizat pentru verificarea automată a teoremelor , pentru funcționarea motoarelor de inferență și a altor aplicații în domeniul inteligenței artificiale . Opusul înlănțuirii înapoi este înlănțuirea înainte . [1]
În jocul de teorie , acest tip de raționament se numește inducție înapoi și constă în căutarea de (simple) subgames pentru a găsi soluția jocului de pornire. În șah , în special, se numește analiză retrogradă .
În programarea logică , înlănțuirea înapoi este implementată utilizând rezoluția SLD . [2]
Operațiune
Înlănțuirea înapoi începe de la o listă de obiective (sau ipoteze) și gândește „înapoi”, pornind de la consecințele regulilor de inferență disponibile și verificând dacă premisele sunt (recursiv) cunoscute ca fiind adevărate. Dacă există un fapt sau un set de fapte care fac premise adevărate (recursiv), atunci se verifică ipoteza de plecare.
Deoarece obiectivele inițiale determină alegerea regulilor de inferență, metoda este definită ca „ orientată spre obiective ”, spre deosebire de metoda de înlănțuire înainte, care este definită ca „ bazată pe date ”.
Exemplu
Să presupunem că scopul este de a găsi culoarea unui anumit animal pe nume Fritz, știind că gâfâie și mănâncă muște și cunoaște următoarele reguli de inferență:
- Dacă X scârțâie și X mănâncă muște, atunci X este o broască.
- Dacă X cântă și X cântă, atunci X este un canar.
- Dacă X este o broască, atunci X este verde.
- Dacă X este un canar, atunci X este galben.
Să presupunem că următoarele fapte sunt adevărate:
- Fritz scârțâie
- Fritz mănâncă muște
- Fritz mănâncă muște
Motivând prin înlănțuire înapoi, motorul de inferență poate deduce că Fritz este verde prin următoarea serie de pași:
- Deoarece este posibil să unificăm obiectivul de plecare cu consecința regulii nr. 3 (în special când „Fritz este verde”), înlocuim în ultimul X cu Fritz, obținând o nouă ipoteză și anume:
- Fritz este o broască
- Deoarece scopul „Fritz este o broască” se unifică cu consecința regulii nr. 1, înlocuim în cel din urmă X cu Fritz, obținând două noi ipoteze și anume:
- Fritz scârțâie
- Fritz mănâncă muște
- Verificăm dacă obiectivele „Fritz scârțâie” și „Fritz mănâncă muște” sunt adevărate, deoarece sunt prezente printre faptele cunoscute. În consecință, întregul lanț de obiective este îndeplinit per modus ponens și, în special, obiectivul de pornire este verificat.
Rețineți că:
- în general, nu toate regulile inferenței sunt necesare pentru a testa ipoteza;
- obiectivul este întotdeauna făcut să corespundă unei consecințe afirmative (și nu negative, ca în modus tollens );
- premisele nu sunt implicate de consecințe (altfel s-ar recadea în eroarea afirmării consecințelor ), dar la rândul lor vor deveni obiective noi de verificat.
Notă
- ^ (EN) Edward Feigenbaum, The Rise of the Expert Company , Times Books, 1988, p. 317 , ISBN 0-8129-1731-6 .
- ^ (EN) Kaustuv Chaudhuri, Frank Pfenning și Greg Price, O caracterizare logică a înlănțuirii înainte și înapoi în metoda inversă, în Proceedings of the International Joint Conference on Automated Reasoning (IJCAR) 2006 Automated Reasoning, Lecture Notes in Computer Science, vol. . 4130, pp. pp. 97-111, DOI : 10.1007 / 11814771_9 , ISBN 978-3-540-37187-8 .
