Глава
Рождение европейской философии истории и логико-темпоральные схемы ренневизантийских авторов
В главе коллективной монографии проводится сопоставление темпоральных логик позднего неоплатонизма и раннехристианской традиции; обсуждаются проблемы генезиса представления о времени как о структуре, образованной рядом моментов-кайрос, каждый из которых может оказаться точкой разрыва временного ряда.
В книге
Книга содержит основные сведения из формально-логических систем. Это функции алгебры логики (булевы функции), теорема Поста о функциональной полноте, k-значные логики, производные булевых функций, аксиоматические исчисления высказываний, предикатов, секвенций, резолюций и язык программирования Пролог. Рассматриваются монадическая логика, конечные автоматы и представимые ими языки, темпоральная логика, аксиоматический язык программирования OBJ3. В основу книги положен многолетний опыт преподавания авторами дисциплины «Дискретная математика» на факультете бизнес-информатики, на факультете компьютерных наук Национального исследовательского университета Высшая школа экономики и на факультете автоматики и вычислительной техники Национального исследовательского университета Московский энергетический институт. Книга предназначена для студентов бакалавриата, обучающихся по направлениям 09.03.01 «Информатика и вычислительная техника», 09.03.02 «Информационные системы и технологии», 09.03.03 «Прикладная информатика», 09.03.04 «Программная инженерия», а также для ИТ-специалистов и разработчиков программных продуктов.
В издании представлен новый перевод «Послания к юношам» свт. Василия Великого (IV в.), снабженный параллельным греческим текстом и подробными комментариями к нему. Во вступлении подробно рассмотрены исторический контекст создания послания и его литературные особенности, очерчен круг античных авторов, на которых опирался святитель при работе над текстом, а также проведено сравнение с двумя другими «посланиями об образовании», написанным в Каппадокии в тот же период. Издание предназначено как студентам-филологам и историкам, так и всем, кто интересуется историей образования и раннего христианства.
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя среда воздействует на систему, и откликов (действий), которые вырабатывает или исполняет система в ответ на внешние воздействия. Поэтому при верификации некоторых видов реагирующих систем элементарными свойствами становятся множества конечных последовательностей действий. Это обстоятельство должно быть также учтено при разработке формального языка спецификаций поведения таких систем. В данной статье рассмотрена задача формальной верификации реагирующих систем, моделируемых конечными автоматами-преоб\-разователями. Для спецификации их поведения предложен новый вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для представления элементарных свойств вычислений, а также для параметризации темпоральных операторов. Установлено, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях разрешима.
В истории восприятия интеллектуального наследия Оригена русскими богословами и философами последних столетий выделяются несколько ключевых моментов и несколько ключевых фигур. Это, прежде всего, Григорий Сковорода (1722–1794), Владимир Соловьёв (1853–1900), Сергей Булгаков (1871–1944), Николай Бердяев (1874–1948) и Георгий Флоровский (1893–1979). Значимость этих авторов для нашего исследования определяется сочетанием трёх обстоятельств: (1) ключевой ролью названных мыслителей в эволюции русской богословской и философской мысли и (2) тем фактом, что их собственная интеллектуальная эволюция, а также (3) восприятие их идей современниками и/или более поздними исследователями осуществлялись в тесной связи с проблемой Оригена. Таким образом, процесс восприятия интеллектуального наследия Оригена в России оказался в существенной степени обусловлен теми спорами, которые велись и ведутся вокруг ключевых представителей так называемой «русской религиозной философии».
О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Мы полагаем, что для формального описания поведения реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционная темпоральная логика линейного времени LTL. В этой работе рассматривается новый язык формальных спецификаций LP-LTL, представляющий собой расширение темпоральной логики LTL, специально разработанное для описания свойств вычислений автоматов-преобразователей. Темпоральные операторы в формулах LP-LTL снабжены параметрами, в качестве которых используются множества слов (языки), описывающие потоки сигналов управления, поступающих на вход реагирующей системы. Базовые предикаты в формулах LP-LTL также определяются языками в алфавите элементарных действий; эти языки описывают ожидаемую реакцию системы в ответ на воздействия окружающей среды. В более ранних работах авторов этой статьи изучалась задача верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами логик LP-LTL и LP-CTL. Было показано, что для обеих логик эта задача алгоритмически разрешима. Цель данной работы — оценить выразительные возможности логики LP-LTL и сравнить ее с широко известными логиками, применяющимися в информатике для спецификации реагирующих систем. В логике LP-LTL были выделены два фрагмента LP-1-LTL и LP-n-LTL. Нам удалось установить, что язык спецификаций LP-1-LTL более выразителен, чем LTL, в то время как фрагмент LP-n-LTL обладает точно такими же выразительными возможностями, что и монадическая логика второго порядка S1S.
В статье в качестве формальной модели последовательных реагирующих систем была предложена модель вычислений конечных автоматов-преобразователей, работающих над полугруппами действий. Для спецификации поведений таких автоматов был предложен специальный вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для параметризации темпоральных операторов. В этой же статье было показано, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях, работающих над свободными полугруппами, разрешима со сложностью по времени, оцениваемой двойной экспонентой от размера проверяемой формулы.
Я показываю, что в рамках учения свт. Григория Нисского развиваются две стратегии построения иерархии сущего: стратегия, предполагающая родовидовые разделения и «все существующее» в качестве вершины иерархии, и стратегия, предполагающая в качестве вершины нетварную природу. Далее я исследую тему иерархии сущего, развиваемую свт. Григорием в 8-й гл. трактата «Об устроении человека» согласно первой из различенных мною стратегий. Я анализирую развитие мысли Григория и выделяю в рамках этой темы у Григория четыре дискурса: антропологический, космогонический, логический и натурфилософский. Я рассматриваю проводимую Григорием тему эволюционного восхождения природы в направлении возрастания жизненной силы природных видов от неодушевленного сущего к человеческому существу, в соответствие с описываемым в Библии порядком творения, вместе со связанной с ней темой родовидовой иерархии (разделения сущего), и исследую влияние предшествующих Григорию авторов на развитие им этих тем. Полемизируя с позицией К. Рейнхардта, Г. Ладнера, Д. Баласа и ряда других исследователей о влиянии учения Посидония на тему иерархии сущего у Григория, я утверждаю, что мнение о влиянии Посидония недостаточно обосновано. Я делаю краткий обзор темы родовидовых разделений у некоторых античных авторов и прихожу к выводу о непосредственном влиянии древа Порфирия на тему разделения сущего у Григория. Также я нахожу у Григория в этом отношении аристотелевскую, платоническую и особенно стоическую линии, предполагая, что именно последняя проявляется, когда Григорий ставит «существующее» на вершину родовидового разделения. Я анализирую общее и отличное между древом Порфирия и иерархией природного сущего у Григория. В отличие от предыдущих исследователей, указывавших только на их близость, я показываю, что имеются также и расхождения между порядком ступеней в этих иерархиях. Я прихожу к выводу, что Григорий изменил порядок ступеней иерархии по сравнению с порфириевским, чтобы согласовать расхожую для его времени логико-философскую схему разделения сущих с логикой описываемого в Библии порядка творения, т.е. желая достичь синтеза между библейским и школьным античным описаниями порядка природного сущего. Наконец, я предполагаю непосредственное влияние учения Аристотеля на тему восходящего порядка природы у Григория, отмечая и различие между ними.