Искусственный интеллект

Потребуется также следующая аксиома единственности имен: Назначить (студент, размер^стипендии) = Назначить (студент1, размер стипендии') з студент = студент' л размер стипендии = = размер^стипендии''. Поиск ответов на запросы к ситуационной Дейталог-программе осуществляется традиционным прямым или обратным выводом, стратегии которого рассмотрены в главе 8 и других главах. При доказательстве же целостности обычно используют индукционные аксиомы, с одной из которых мы подробно ознакомились и привели в главе 9 детальное доказательство на ее основе корректности программы. Применяются и другие индукционные аксиомы. В частности, для проверки целостности ситуационной Дейталог-программы часто применяется двойная индукционная аксиома. Рассмотрим, как может быть использована эта аксиома для доказательства целостности ситуационной Дейталог-программы.