Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

в идеальном случае верификация проводится полностью автоматически (на ранее построенной системе). Однако на практике она требует содействия исследователя. Если результаты верификации отрицательны, то пользователю может предоставляться трасса, содержащая ошибку. Анализ ошибки позволяет исследователю модифицировать проверяемую систему и повторно провести ве­ рификацию. На начальном этапе системы верификации были способны проверять сис­ темы, содержаш,ие примерно 10^ состояний. В настояш,ее время улучшения, внесенные в технологию верификации, позволяют расширить границы по числу состояний [16]. § 10. Приложения неклассических логик В настояш,ее время наблюдается значительный рост интереса к некласси­ ческим логикам, что связано в том числе и с развитием компьютерных инфор­ мационных технологий. Языки неклассических логик предоставляют богатые выразительные средства, благодаря чему сами логики находят массу приложе­ ний в различных областях знания. Своего рода «обратной стороной» вырази­ тельности языка неклассических логик является их высокая сложность: хотя почти все стандартные неклассические логики разрешимы, тем не менее, про­ блема их разрешения является «практически неразрешимой». Так, уже пробле­ ма выполнимости булевых формул NP-полна, а проблема разрешения многих неклассических логик не только NP-, а еш,е сложнее. Это, в частности, означает, что выяснение выводимости в некоторой логике даже сравнительно несложных формул (скажем, всего лишь от ста переменных) может потребовать (с исполь­ зованием известных на данный момент алгоритмов и имеюш,ихся компьютеров с их вычислительными возможностями) времени, не укладываюш,егося в рамки человеческой жизни. Получается, что такое, казалось бы, хорошее свойство не­ классических логик, как разрешимость, оказывается мало что даюш,им для при­ ложений. Тем не менее, нетрудно заметить, что в приложениях никогда не использу­ ется вся логика; используется только её часть, фрагмент. При этом реально ис­ пользуемые фрагменты образованы формулами от конечного (и даже можно считать, заранее ограниченного) множества переменных. В результате получа­ ем, что для приложений не так уж и актуальна проблема выполнимости формул для всей логики, а актуальна лишь аналогичная проблема для соответствуюш,их фрагментов. Логический подход к созданию новых информационных технологий явля­ ется в настоящее время, пожалуй, наиболее распространенным при разработке интеллектуальных и экспертных систем в различных предметных областях. В этих исследованиях двоичная классическая логика обычно замещается какой- 212