5.1.	Методы теоретической информатики в проблеме  автоматического  
        построения  алгоритмов (структурная трансформация и синтез)
5.2.	94-01-00944
5.3.	01.1994
5.4.	12.1996
5.5.	РФФИ
5.6.	Нагорный Николай Макарович (ВЦ РАН)
5.7.	Гавриленко Юрий Вячеславович (ВЦ РАН)
5.7.	Хомич Валентин Иванович (ВЦ РАН)
5.8.	русский
5.9.	01-202, РФФИ
5.9.	01-208, РФФИ
5.10.1.	алгоритм, псевдобулева алгебра, интуиционистское 
        пропозициональное исчисление,  суперинтуиционистское 
        пропозициональное  исчисление,  интуиционистская  
        пропозициональная логика,  суперинтуиционистская пропозициональная  
        логика, отделимость,  изоморфная  вложимость,  дедуктивный синтез
        программ,  интуиционизм, клиниевская реализуемость, 
        конструктивная семантика, непротиворечивость арифметики
5.10.2.	
5.11.1.	 В ходе выполнеия проекта были получены следующие
         результаты:

        а) исследовалась одна  модификация  введенного  С.К.Клини
        понятия реализуемой логико-арифметической формулы, в свое
        время фактически предвосхитившего  основную  проблематику
        автоматического извлечения алгоритмов из интуиционистских
        выводов описывающих их спецификаций  (теорема  Нельсона);
        для  данной  модификации  удалось доказать аналог теоремы
        Нельсона в применении к классической формальной арифметике,  
        откуда следует ее непротиворечивость; доказательство
        выдержано в духе "логического консенсуса",  а именно, оно
        "нейтрально" по отношению к основным современным логическим 
        концепциям - к традиционной аристотелевской,  а также
        к интуиционистской и конструктивной логикам; были 
        проанализированы  также  оставшиеся  неопубликованными   работы
        А.А.Маркова,  относящиеся к периоду его занятий клиниевской 
        реализуемостью,  и сформулирован ряд важнейших возникающих 
        в связи с этими работами проблем;

        б) исследовалась проблема изоморфной вложимости некоторых
        обобщений псевдобулевых алгебр, являющихся моделями 
        интуиционистской пропозициональной логики,  используемой  при
        автоматическом синтезе программ;  для этих обобщений были
        получены критерии изоморфной вложимости друг в друга; был
        описан  полный  по  вложению класс конечных псевдобулевых
        алгебр; исследовалась связанная с задачей автоматического
        синтеза алгоритмов проблема отделимости для суперинтуиционистских
        пропозициональных логик; дополнительные аксиомы
        этих логик трактуются как условия, налагаемые на исходные
        данные синтезируемых программ;  отделимость такой  логики
        обеспечивает  успех  поиска  вывода  в рассматриваемом ее
        фрагменте, что является одним из этапов синтеза программ;
        были получены критерии отделимости нормализуемых 
        суперинтуиционистских пропозициональных логик; была доказана
        отделимость нормализуемых табличных логик; изучалось свойство
        суперинтуиционистских  пропозициональных  исчислений,
        связанное с отделимостью этих исчислений; для нетривиального
        класса таких  исчислений  получен  критерий  наличия
        данного свойства;  с помощью него было доказано существование
        алгоритма,  распознающего обладающие им  исчисления
        среди исчислений рассматриваемого класса.

5.11.2.