Зворотний вивід
 | Ця стаття містить перелік джерел, але походження окремих тверджень у ній залишається незрозумілим через практично повну відсутність виносок. (липень 2020) |
Зворотний вивід (або зворотне міркування) є метод отримання висновку, який працює в зворотному напрямку від мети. Він використовується в автоматизованому доведенні теорем, машинному висновуванні та інших напрямках штучного інтелекту, також спостерігається у приматів.
В теорії ігор застосування зворотного виводу для під-ігор[en], з метою знайти рішення гри, називається зворотною індукцією. У шахах даний метод називається ретроспективним аналізом, він використовується для створення баз таблиць для ендшпіля у комп'ютерних шахах.
Зворотний вивід здійснюється у логічному програмуванні за допомогою SLD-резолюції. Обидва правила базуються на правилі виводу modus ponens. Це один з двох найбільш часто використовуваних методів міркування при роботі з правилами висновування та логічними наслідками, є протилежним до прямого виводу. Системи зворотного виводу, наприклад, Пролог, зазвичай використовують стратегію пошуку в глибину.
Зворотний вивід починається з переліку цілей (або гіпотез) і працює в зворотному напрямку від висновку до антецеденту, щоб побачити, чи доступні дані, які будуть підтримувати будь-який з цих висновків.
Механізм логічного виводу, що використовує зворотний вивід, шукає серед правил виводу перше правило, у якого висновок (частина Тоді) відповідає поставленій меті. Якщо невідомо, чи набуває антецедент (частина Якщо) цього правила логічного значення "істина", тоді антецедент цього правила додається до списку цілей. (для того, щоб мета підтвердилася, необхідно також отримати дані для підтвердження цього нового правила).
Наприклад, метою є визначення кольору тварини, яка квакає і їсть мух. База правил виводу містить такі чотири правила:
- Якщо X квакає і їсть мух - Тоді X - це жаба
- Якщо X щебече і співає - Тоді X - це канарка
- Якщо X - жаба - Тоді X має зелений колір
- Якщо X - канарка - Тоді X має жовтий колір
По базі правил виводу буде здійснено пошук, будуть вибрані правило №3 і №4, бо їх висновки (Тоді тварина має зелений колір, Тоді тварина має жовтий колір) відповідають меті (визначити колір тварини). Поки ще невідомо, чи є тварина жабою або канаркою, тому обидва правила будуть додані в список цілей. По базі правил виводу знову здійснюється пошук, цього разу механізм обере правила перші два правила, тому що їх висновки (Тоді тварина - це жаба, Тоді тварина - це канарка) відповідає цілям, які були щойно додані в список. Антецедент (Якщо тварина квакає і їсть мух), як відомо, є істинним, тому можна зробити висновок, що тварина є жабою і не канаркою. Мету визначення кольору тварини тепер досягнуто (тварина має зелений колір, якщо це жаба, і жовтий, якщо це канарка, але тварина є жабою, оскільки вона квакає і їсть мух, тому тварина має зелений колір).
Зверніть увагу, що цілям завжди відповідають висновки, у яких пізніше антецеденти розглядаються як нова мета. Зрештою, антецедентам повинні відповідати відомі факти (вони, як правило, визначаються як висновки, у яких завжди істинний антецедент). Таким чином, правилом висновування, яке використовується є modus ponens.
Оскільки саме список цілей визначає, які правила вибирати і використовувати, цей метод називається методом, керованим метою, на відміну від прямого виводу, що є методом, керованим даними. Зворотний вивід часто використовується в експертних системах.
Мови програмування, такі як Пролог, Knowledge Machine і ECLiPSe підтримують метод зворотного виводу в своїх механізмах виводу.
Стюарт Рассел, Питер Норвиг Искусственный интеллект: современный подход. — М.: Вильямс, 2007. С. 1424. ISBN 0-13-790395-2
- Приклади зворотнього виводу [Архівовано 21 березня 2012 у Wayback Machine.]