Russell — это логический каркас, предназначенный для спецификации и реализации дедуктивных систем. Он является языком высокого уровня по отношению к языку Metamath, поэтому он наследует основания Metamath, то есть не зависит от какого либо конкретного формального исчисления, но является чистым логическим каркасом. Основная разница между Russell и Metamath заключается в языке доказательств и подходу к синтаксису: доказательства в Russell имеют декларативную форму, то есть содержат явно выражения, составляющие доказательство, а синтаксические правила грамматики разделены в Russell с содержательными правилами вывода.
Russell реализован на c++14 и распространяется по лицензии GPL v3. Репозиторий содержит транслятор из Metamath в Russell и обратно. Оригинальная база теорем Metamath (почти 30 000 теорем) транслируется в Russell, верифицируется, транслируется обратно в Metamath и верифицируется оригинальным верификатором Metamath. Адрес репозитория: https://github.com/dmitry-vlasov/russell.
В статье мы описываем подход для формальной проверки параллельных и распределенных программ на C#. Мы используем технологию Microsoft Roslyn для получения синтаксической и семантической информации об интересных конструкциях в реальном коде, чтобы сгенерировать соответствующий код на модельном языке Promela, предназначенном для описания взаимодействующих систем на основе акторов. Затем мы проверяем проблемы параллельного и распределенного кода, используя предопределенные предикаты LTL для модельной программы. Мы можем определять проблемы гонки данных, неправильное использование блокировок, возможные взаимоблокировки в распределенных сервисных взаимодействиях с использованием подхода проверки модели. Описанный метод может быть использован для построения статического анализатора для платформы .NET.
Описывается построение и дедуктивная верификация предикатной программы бинарного поиска, идентичной программе bsearch на языке Си из библиотеки ОС Linux. В языке предикатного программирования определяются новые конструкции для произвольных типов в качестве параметров программ. Для объектов произвольного типа вводятся трансформации кодирования через указатели.
В статье представлены результаты исследования изменений, происходящих в тематических кластерах, построенных на коллекции текстов конференций предметной области Argument mining. Выявление терминов, установление связей между ними и тематическая кластеризация проведены с помощью сторонних программных средств, позволяющей извлекать термины в форме именных словосочетаний, проводить их кластеризацию на базе алгоритма, основанного на применении функции модулярности. Приводится оценка качества полученных кластеров по трем критериям. Трансформацию терминологического состава кластеров во времени предлагается анализировать с помощью ориентированных графов, построенных на основе критерия, который позволяет фиксировать наиболее важные изменения. Терминологическая лексика выявленных тематических кластеров характеризует отдельные направления, в которых ведутся исследования, а трансформация терминологического состава кластеров во времени демонстрирует смещение интересов.