Cтраница 3
Для общегосударственной программы создания, развития и эффективного использования вычислительной техники огромное значение имеют научные исследования, проводимые в СО АН СССР в области физико-математических и технических наук. Среди других достижений в этой области академик В.А. Коптюг назвал работы Института математики, где важные теоретические результаты получены в области дифференциальных уравнений в частных производных, а также предложены и обоснованы допускающий гарантированную оценку точности алгоритм приведения симметрических матриц к диагональному виду и алгоритм расчета сингулярного разложения произвольных матриц. [31]
В статье Some trends in automated reasoning ( Некоторые тенденции в автоматическом поиске вывода) описан алгоритм автоматического доказательства теорем исчисления предикатов первого порядка, предложенный А. Г. Драгалиным и реализованный группой его сотрудников в Дебрецене. Общая схема соответствует методу метапеременных. Затем матрица В приводится к эквивалентной конъюнктивной нормальной форме - кластеру fcj, состоящему из дизъюнктов. Эта процедура полна для исчисления высказываний. U v может быть превращена в тавтологию некоторой подстановкой термов вместо метапеременных. Для этого ищется наиболее общий унификатор, превращающий все дизъюнкты из fc - в тавтологии. Возможности этой программы примерно соответствовали возможностям современных ей не-резолюционных программ. Отличия от этих программ включали оптимизированный алгоритм приведения к конъюнктивной нормальной форме и поэтапный ( а не глобальный) поиск окончательной подстановки термов вместо метапеременных. [32]