Wnioskowanie w tył
Z Wikipedii
Wnioskowanie w tył polega na tym, że wychodzimy od tego, co chcemy udowodnić i idziemy w kierunku aksjomatów.
Czyli żeby udowodnić X, udowadniamy 
, 
i tak dalej, aż dojdziemy do aksjomatów. Oczywiście nie wiemy czy idziemy w dobrym kierunku, ale ponieważ aksjomaty znamy z góry, możemy zaplanować algorytm tak, żeby raczej zachowywał odpowiedni kierunek. Jest to duża przewaga nad wnioskowaniem w przód, jako że w tamtym przypadku znajomość aksjomatów okazuje się niewystarczająca do skutecznej optymalizacji.
