01.1994 - 12.1996 ,    Код проекта: 94-01-00944  Описание В ходе выполнеия проекта были получены следующие результаты: а) исследовалась одна модификация введенного С.К.Клини понятия реализуемой логико-арифметической формулы, в свое время фактически предвосхитившего основную проблематику автоматического извлечения алгоритмов из интуиционистских выводов описывающих их спецификаций (теорема Нельсона); для данной модификации удалось доказать аналог теоремы Нельсона в применении к классической формальной арифмети- ке, откуда следует ее непротиворечивость; доказательство выдержано в духе "логического консенсуса", а именно, оно "нейтрально" по отношению к основным современным логичес- ким концепциям - к традиционной аристотелевской, а также к интуиционистской и конструктивной логикам; были проана- лизированы также оставшиеся неопубликованными работы А.А.Маркова, относящиеся к периоду его занятий клиниевс- кой реализуемостью, и сформулирован ряд важнейших возни- кающих в связи с этими работами проблем; б) исследовалась проблема изоморфной вложимости некоторых обобщений псевдобулевых алгебр, являющихся моделями инту- иционистской пропозициональной логики, используемой при автоматическом синтезе программ; для этих обобщений были получены критерии изоморфной вложимости друг в друга; был описан полный по вложению класс конечных псевдобулевых алгебр; исследовалась связанная с задачей автоматического синтеза алгоритмов проблема отделимости для суперинтуици- онистских пропозициональных логик; дополнительные аксиомы этих логик трактуются как условия, налагаемые на исходные данные синтезируемых программ; отделимость такой логики обеспечивает успех поиска вывода в рассматриваемом ее фрагменте, что является одним из этапов синтеза программ; были получены критерии отделимости нормализуемых суперин- туиционистских пропозициональных логик; была доказана от- делимость нормализуемых табличных логик; изучалось свойс- тво суперинтуиционистских пропозициональных исчислений, связанное с отделимостью этих исчислений; для нетривиаль- ного класса таких исчислений получен критерий наличия данного свойства; с помощью него было доказано существо- вание алгоритма, распознающего обладающие им исчисления среди исчислений рассматриваемого класса.  Ключевые слова алгоритм, псевдобулева алгебра, интуиционистское пропози- циональное исчисление, суперинтуиционистское пропозицио- нальное исчисление, интуиционистская пропозициональная логика, суперинтуиционистская пропозициональная логика, отделимость, изоморфная вложимость, дедуктивный синтез программ, интуиционизм, клиниевская реализуемость, конс- труктивная семантика, непротиворечивость арифметики Специальность РФФИ 01-202 Искусственный интеллект и принятие решений , 01-208 Теория программирования