• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • Национальный исследовательский университет «Высшая школа экономики»
  • Публикации ВШЭ
  • Статьи
  • Bar-Hillel Theorem Mechanization in Coq
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Приоритетные направления
  • бизнес-информатика
  • государственное и муниципальное управление
  • гуманитарные науки
  • инженерные науки
  • компьютерно-математическое
  • математика
  • менеджмент
  • право
  • социология
  • экономика
по году
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • еще
Тематика
Новости
16 июня 2026 г.
Публичность ученого: идеальная мера
Еще недавно публичность для ученого считалась чем-то факультативным – полезным, но необязательным. Сегодня она все чаще встроена в научную работу. Не потому, что «надо быть в медиа», а потому что без внешней проявленности исследования могут просто не найти ни аудитории, ни партнеров, ни продолжения. Об этом в статье для IQ Media размышляет эксперт по научным коммуникациям, доцент факультета географии Высшей школы экономики Надежда Пупышева.
15 июня 2026 г.
Ученые ВШЭ выяснили, кто чаще проверяет информацию в интернете
Исследователи НИУ ВШЭ выяснили, как российские интернет-пользователи проверяют сомнительную информацию и что заставляет их это делать. Оказалось, что более половины, заподозрив обман, пытаются отыскать первоисточник. А определяющими факторами в деле проверки становятся возраст, место жительства, социальное положение, навыки работы с информацией и использование ИИ. Результаты опубликованы в журнале «Мониторинг общественного мнения: экономические и социальные перемены».
15 июня 2026 г.
<a>Институт робототехнических систем ВШЭ запустил научно-технический семинар
Институт робототехнических систем (ИРС) ВШЭ запустил новый ежемесячный формат — Научно-технический семинар. Он объединяет сотрудников института, приглашенных экспертов, студентов, исследователей и представителей других подразделений НИУ ВШЭ для обсуждения актуальных задач мехатроники, робототехники и киберфизических систем.

 

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!

Публикации
  • Книги
  • Статьи
  • Главы в книгах
  • Препринты
  • Верификация публикаций
  • Расширенный поиск
  • Правила использования материалов
  • Наука в ВШЭ

?

Bar-Hillel Theorem Mechanization in Coq

Lecture Notes in Computer Science. 2019. Vol. 11541. P. 264–281.
Grigorev S., Bozhko S., Хатбуллина Л. Р.
Научное направление: Компьютерные науки Математика
Приоритетные направления: компьютерно-математическое
Язык: английский
Полный текст
DOI
Текст на другом сайте
Ключевые слова: closureContext-free languagesformal languagesregular languagecoqBar-Hillel theoremintersection
Похожие публикации
Proceedings of the 19th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers)
Association for Computational Linguistics, 2026.
Добавлено: 14 июня 2026 г.
Proceedings of the 6th Workshop on Computational Approaches to Discourse, Context and Document-Level Inferences (CODI 2025)
Strube M., Braud C., Hardmeier C. и др., Suzhou: Association for Computational Linguistics, 2025.
Добавлено: 11 июня 2026 г.
On the Ramsey Number R(K_{1,s},P_t)
Kh. Kh. Abdullin, D. B. Mokeev, D. S. Taletskii, Mathematical notes 2026 Vol. 119 No. 1 P. 3–7
Добавлено: 10 июня 2026 г.
TreeDQN: Sample-efficient off-policy reinforcement learning for combinatorial optimization
Sorokin D., Kostin A., Савченко Л. В. и др., Knowledge-Based Systems 2026 Vol. 348 Article 116258
Добавлено: 10 июня 2026 г.
Microbial diversity and production of milk spirit using traditional Buryat fermentation and distillation technologies
Namsaraev Z., Nanzatov B., Козлова А. Д. и др., Scientific Reports 2026 Vol. 16 No. 1 Article 17769
Дистиллированные кисломолочные напитки встречаются в пищевой промышленности редко, несмотря на повсеместное распространение растительных спиртных напитков. В настоящее время производство крепких дистиллированных алкогольных напитков из кисломолочных продуктов с использованием традиционных технологий известно лишь среди монголоязычных народов и их сибирских соседей. Данное исследование представляет собой первый междисциплинарный анализ дарасуна, традиционного бурятского спиртного напитка, изготавливаемого из кисломолочного напитка ...
Добавлено: 10 июня 2026 г.
Artificial intelligence and digital twins for failure prediction in data center cooling systems: a comprehensive literature review (2018–2026)
Butorova A., Bobakov V., Sergeev A. и др., European Physical Journal: Special Topics 2026 P. 1–19
Добавлено: 10 июня 2026 г.
ML-based Fast Simulation of FARICH Responses
Шипилов Ф. А., Barnyakov A., Ivanov A. и др., / Series Physics "arxiv.org". 2026.
Добавлено: 19 мая 2026 г.
Natural hazard database from Internet publications: text mining with a large language model
Деркачева А. А., Сакиркина М. А., Краев Г. Н. и др., /. 2026.
Добавлено: 28 апреля 2026 г.
Algorithmic overlaps as thermodynamic variables: from local to cluster Monte Carlo dynamics in critical phenomena
Пиле Я. Э., Deng Y., Щур Л. Н., / Series arXiv "math". 2026. No. 2604.10254.
Добавлено: 20 апреля 2026 г.
Using predefined vector systems to speed up neural network multimillion class classification
Gabdullin N., Андросов И. А., / Series Computer Science "arxiv.org". 2026.
Добавлено: 2 апреля 2026 г.
Iterative Ricci-Foster Curvature Flow with GMM-Based Edge Pruning: A Novel Approach to Community Detection
Сорокин К. С., Бекетов М. Е., Онучин А. и др., / arxiv.org. Серия cs.SI "Social and Information Networks ". 2025.
Обнаружение сообществ в сложных сетях — фундаментальная проблема, открытая для новых подходов в различных научных областях. Мы представляем новый метод обнаружения сообществ, основанный на потоке Риччи на графах. Наша техника итеративно обновляет веса ребер (их метрические длины) в соответствии с их (комбинаторной) версией кривизны Риччи Фостера, вычисленной на основе эффективного расстояния сопротивления между узлами. Известно, ...
Добавлено: 15 января 2026 г.
Implementing Transport Coding in OMNeT++ for Message Delay Reduction
Петрованов И. С., Сергеев А. В., / Series Computer Science "arxiv.org". 2025. No. 2512.18332.
Добавлено: 24 декабря 2025 г.
Hessian-based lightweight neural network for brain vessel segmentation on a minimal training dataset
Меньшиков И. А., Бернадотт А. К., Елфимов Н. С., / Series arXie "Statistical mechanics". 2025.
Добавлено: 1 декабря 2025 г.
Determining the boundary of dynamical chaos in the generalized Chirikov map via machine learning
Чернышов Д. П., Сатанин А. М., Щур Л. Н., / Series arXiv "math". 2025.
Добавлено: 21 ноября 2025 г.
Эффективный алгоритм торговли на фондовом рынке: ретроспективный анализ, основанный на данных по S&P-500.
Рубчинский А. А., Чубарова Д. А., / Series WP7 "Математические методы анализа решений в экономике, бизнесе и политике". 2025. No. WP7/2025/01.
Добавлено: 9 ноября 2025 г.
On Decidability of Theories of Regular Languages
Sergey Dudakov, Karlov B., Theory of Computing Systems 2021 Vol. 65 No. 3 P. 462–478
Добавлено: 12 ноября 2023 г.
О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...
Добавлено: 17 января 2022 г.
Octagonal picture languages
Govindaraj R., Махендран А., International Journal of Reasoning-based Intelligent Systems 2018 Vol. 3 No. 4 P. 197–203
Добавлено: 24 ноября 2021 г.
A Linear-Time Simulation of Deterministic d-Limited Automata
Рубцов А. А., , in: Developments in Language Theory: 25th International Conference, DLT 2021, Porto, Portugal, August 16–20, 2021, Proceedings.: Switzerland: Springer International Publishing, 2021. P. 342–354.
Добавлено: 28 сентября 2021 г.
Developments in Language Theory: 25th International Conference, DLT 2021, Porto, Portugal, August 16–20, 2021, Proceedings
Switzerland: Springer International Publishing, 2021.
Добавлено: 28 сентября 2021 г.
Context-Free Languages and Associative Algebras with Algebraic Hilbert Series
Пионтковский Д. И., La Scala R., Springer INdAM Series 2021 Vol. 44 P. 279–289
Добавлено: 3 апреля 2021 г.
Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday
Cham: Springer, 2020.
Добавлено: 25 ноября 2020 г.
Using an extension of CTL* for specification and verification of sequential reactive systems
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21–32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 2020 г.
Repairing and mechanising the JavaScript relaxed memory model
Watt C., Pulte C., Подкопаев А. В. и др., , in: PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation.: NY: Association for Computing Machinery (ACM), 2020. P. 346–361.
Добавлено: 19 августа 2020 г.
  • О ВЫШКЕ
  • Цифры и факты
  • Руководство и структура
  • Устойчивое развитие в НИУ ВШЭ
  • Преподаватели и сотрудники
  • Корпуса и общежития
  • Закупки
  • Обращения граждан в НИУ ВШЭ
  • Фонд целевого капитала
  • Противодействие коррупции
  • Сведения о доходах, расходах, об имуществе и обязательствах имущественного характера
  • Сведения об образовательной организации
  • Людям с ограниченными возможностями здоровья
  • Единая платежная страница
  • Работа в Вышке
  • ОБРАЗОВАНИЕ
  • Лицей
  • Довузовская подготовка
  • Олимпиады
  • Прием в бакалавриат
  • Вышка+
  • Прием в магистратуру
  • Аспирантура
  • Дополнительное образование
  • Центр развития карьеры
  • Бизнес-инкубатор ВШЭ
  • Образовательные партнерства
  • Обратная связь и взаимодействие с получателями услуг
  • НАУКА
  • Научные подразделения
  • Исследовательские проекты
  • Мониторинги
  • Диссертационные советы
  • Защиты диссертаций
  • Академическое развитие
  • Конкурсы и гранты
  • Внешние научно-информационные ресурсы
  • РЕСУРСЫ
  • Библиотека
  • Издательский дом ВШЭ
  • Книжный магазин «БукВышка»
  • Типография
  • Медиацентр
  • Журналы ВШЭ
  • Публикации
  • http://www.minobrnauki.gov.ru/
    Министерство науки и высшего образования РФ
  • https://edu.gov.ru/
    Министерство просвещения РФ
  • http://www.edu.ru
    Федеральный портал «Российское образование»
  • https://elearning.hse.ru/mooc
    Массовые открытые онлайн-курсы
  • НИУ ВШЭ1993–2026
  • Адреса и контакты
  • Условия использования материалов
  • Политика конфиденциальности
  • Правила применения рекомендательных технологий в НИУ ВШЭ
  • Карта сайта
Редактору