?
Bar-Hillel Theorem Mechanization in Coq
Lecture Notes in Computer Science. 2019. Vol. 11541. P. 264–281.
Grigorev S., Bozhko S., Хатбуллина Л. Р.
Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verifica- tion, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theo- rem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.
Priority areas:
IT and mathematics
Language:
English
Borisov D., Katzarkov Ludmil, Sheshmani A. et al., American Journal of Mathematics 2026 Vol. 148 No. 4 P. 1075–1101
It is shown that there are globally defined Lagrangian distributions on the stable loci of derived \mathrm{Quot}-stacks of coherent sheaves on Calabi--Yau four-folds. Dividing by these distributions produces perfectly obstructed smooth stacks with globally defined -1-shifted potentials, whose derived critical loci give back the stable loci of smooth stacks of sheaves in global Darboux form. ...
Added: August 18, 2026
Moshkin A., Fedorov M., Arlazarov V. et al., Algorithms 2026 Vol. 19 No. 7 Article 523
Artificial intelligence (AI) technologies, which are being actively developed in modern medicine today, increase the speed and quality of patient care. This article mainly seeks to demonstrate the use of various options of computer analysis of clinical images to solve practical problems of increasing the efficiency of routine diagnostics using retrospective analysis, as well as ...
Added: August 17, 2026
CHEN Y., Howlett R. J., Tanaka S. et al., Springer, 2026.
The Smart Innovation, Systems and Technologies book series encompasses the topics of knowledge, intelligence, innovation and sustainability. The aim of the series is to make available a platform for the publication of books on all aspects of single and multi-disciplinary research on these themes in order to make the latest results available in a readily-accessible ...
Added: August 16, 2026
Богатырев А. Б., Математический сборник 2023 Т. 214 № 3 С. 106–119
Рассматривается клеточное разбиение пространства модулей вещественных кривых рода 2 с отмеченной точкой на единственном вещественном овале. Клетки перечисляются определенными графами, веса которых описывают комплексную структуру на кривой. Показано, что стягивание ребра графа приводит к корневой особенности естественного отображения из весов графа в пространство модулей кривых. ...
Added: August 14, 2026
Богатырев А. Б., Gendron Q., Успехи математических наук 2023 Т. 78 № 1 С. 209–210
Уравнение Пелля-Абеля — это функциональное уравнение вида P²-DQ² = 1, с заданным многочленом D, свободным от квадратов, и неизвестными многочленами P и Q. Мы показываем, что пространство уравнений Пелля-Абеля с фиксированными степенями D и примитивным решением P является комплексным многообразием. Мы описываем его связные компоненты с помощью эффективно вычислимого инварианта. ...
Added: August 14, 2026
Богатырев А. Б., Transactions of the Moscow Mathematical Society 2024 Vol. 85 No. 2 P. 323–337
The best uniform rational approximation of the Sign function on two intervals separated by zero was explicitly found by E. I. Zolotarëv in 1877. The natural extension of this problem to three bands was solved by E. Stiefel in 1961. We indicate the solutions overlooked by the prominent geometer and study their properties. ...
Added: August 14, 2026
Богатырев А. Б., Успехи математических наук 2026 Т. 81 № 3(489) С. 159–160
Предложена простая и эффективно реализуемая формула для изменения абелевых интегралов (включая их периоды) при вариации образующих классической группы Шоттки, представляющей риманову поврехность. ...
Added: August 14, 2026
Gendron Q., Compositio Mathematica 2025 Vol. 161 No. 7 P. 1483–1511
A Pell–Abel equation is a functional equation of the form P^2-DQ^2=1 , with a given polynomial D free of squares and unknown polynomials P and Q. We show that the space of Pell–Abel equations with the degrees of D and of the primitive solution P fixed is a complex manifold. We describe its connected components ...
Added: August 14, 2026
Yu Z., Wang J., Wang Z. et al., Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 2026 Vol. 384 P. 1–16
The integration of data-driven and knowledge-driven approaches in generative geospatial modelling (GGM) is often hindered by their mathematical incompatibilities. Here, we propose a geometric algebra (GA)-based framework that employs a unified multi-vector representation to fuse heterogeneous data and diverse knowledge. The framework facilitates structured reasoning and hypothesis generation through a task-adaptable, five-stage cycle: representation, reasoning, ...
Added: August 13, 2026
Cham: Springer, 2026.
This book constitutes the proceedings of the 10th International Workshop Empowering Novel Geometric Algebra for Graphics and Engineering, ENGAGE 2025, held in conjunction with Computer Graphics International conference, CGI 2025, in Hong Kong, China, on July 14, 2025.
The 14 full papers included in this volume were carefully reviewed and selected from 16 submissions. The papers ...
Added: August 13, 2026
Ratnikov F., European Physical Journal: Special Topics 2026 P. 1–10
EEG recordings are often affected by the loss or corruption of individual channels due to electrode detachment, poor scalp contact, or external interference. Such channels must be accurately reconstructed before further analysis. In this study, we investigate Next-Generation Reservoir Computing (NG-RC) as a data-driven approach for reconstructing corrupted EEG channels and compare its performance with ...
Added: August 12, 2026
Speranski S. O., Математические заметки 2026 Т. 120 № 3 С. 470–483
We show that, in terms of closure ordinals, many infinitary calculi for ‘first-order’ logics of probability (i.e., for languages similar to those in [Abadi & Halpern 1994]) are as hard as possible: the corresponding closure ordinals coincide with the least non-constructive ordinal, denoted by $\omega_1^{\mathrm{CK}}$. ...
Added: August 12, 2026
Minets M., Krasnozhenov G., Trofimova E. et al., PeerJ Computer Science 2026 Vol. 12 Article e4063
This article presents CAD2TechSpec, a novel framework for automating design processes within computer-aided design (CAD) systems by leveraging multimodal large language models (LLMs). The framework enables the analysis and generation of detailed design specifications, including the automated creation of machining process plans. Our system architecture combines 3D model rendering, dimensionality reduction techniques, and the capabilities ...
Added: August 12, 2026
Мизинов П. В., Journal of Computer Virology and Hacking Techniques 2023 No. 20 P. 383–396
Biometric vein recognition systems are vulnerable to presentation attacks. Traditionally, researchers have used a near-infrared (NIR) drawing of the user’s vascular bed to create a presentation attack instrument (PAI). This paper investigates the feasibility of using free software to capture a venous pattern of the hand without NIR under normal lighting conditions and to create ...
Added: August 11, 2026
Ali S., Bocharnikov V., Ratnikov F. et al., Sensors 2026 Vol. 26 No. 16 Article 5024
Large distributed sensor arrays require repeated recalibration as radiation damage, material aging, gain variation, and readout drift alter channel responses. We studied a high-granularity calorimeter as a large sensor array and addressed unsupervised recalibration from two unpaired datasets: a nominal reference response and an aged response with attenuated cell-wise signals. Aging was modeled by a ...
Added: August 11, 2026
Trubochkina N. K., М.: Издательство «Юрайт», 2026.
This textbook is designed to develop students' holistic understanding of modern production processes and methods for their analysis and management using machine learning technologies. In the context of the fourth industrial revolution, where traditional engineering disciplines are inextricably intertwined with intelligent data processing methods, there is a growing need for specialists capable of integrating knowledge ...
Added: August 8, 2026
Kulev Y., Maksaev A., Promyslov V., Linear Algebra and its Applications 2026 Vol. 730 P. 51–72
The notion of λ-th upper scrambling index was introduced by Huang and Liu in 2010, as a generalization of a notion considered by Akelbek and Kirkland in 2009. For a primitive digraph D, it is defined as the smallest positive integer k such that for every λ vertices of D there exist directed paths of lengths k from these vertices to a common vertex. This ...
Added: August 7, 2026
Kanunnikov A., Promyslov V., Vassilieva E., Electronic Journal of Combinatorics 2024 Vol. 31 No. 3 Article P3.6
Introduced by Goulden and Jackson in their 1996 paper, the matchings-Jack conjecture and the hypermap-Jack conjecture (also known as the b-conjecture) are two major open questions relating Jack symmetric functions, the representation theory of the symmetric groups and combinatorial maps. They show that the coefficients in the power sum expansion of some Cauchy sum for ...
Added: August 7, 2026
Фирсанова В. И., ACM, 2026.
The inclusion of autistic people can be augmented by a mobile app that provides information without a human mediator making information perception more liberating for people in the spectrum. This paper is an overview of a doctoral work dedicated to the development of a web-based mobile tool for supporting the inclusion of people on the ...
Added: August 4, 2026
Ponomarenko A., / Series Computer Science "arxiv.org". 2025.
This paper addresses the challenge of merging hierarchical navigable small world (HNSW) graphs, a critical operation for distributed systems, incremental indexing, and database compaction. We propose three algorithms for this task: Naive Graph Merge (NGM), Intra Graph Traversal Merge (IGTM), and Cross Graph Traversal Merge (CGTM). These algorithms differ in their approach to vertex selection ...
Added: July 30, 2026
Шиманогов И. Н., Vyalyi M., Дискретный анализ и исследование операций 2025 Т. 32 № 4(166) С. 213–230
A well-studied class of algorithmic problems is that of regular realizability: checking the non-emptiness of the intersection of a regular language with a given language. This problem has a natural algebraic interpretation: verifying whether an element of a Boolean algebra belongs to the kernel of a certain homomorphism. This motivates the consideration of an analogous ...
Added: July 12, 2026
Piontkovski D., / Series arXiv "math". 2026.
A noncommutative projective variety is defined, following Artin and Zhang, by a graded coherent algebra 𝐴. The category of coherent sheaves is then the quotient qgr(𝐴) of the category of finitely presented graded modules by the subcategory of torsion modules. We consider the categorical and polynomial entropies of the Serre twist, that is, of the ...
Added: June 23, 2026
Piontkovski D., / Series arXiv "math". 2025.
If a symmetric multilinear algebra is weakly nil, then it is Engel. This result may be regarded as an infinite-dimensional analogue of the well-known Jacobian theorem, which states that if a polynomial mapping has a polynomial inverse, then its Jacobian matrix is invertible. This refines a theorem of Gerstenhaber and partially answers a question posed ...
Added: June 23, 2026
Shipilov F., Barnyakov A., Ivanov A. et al., / Series Physics "arxiv.org". 2026.
A fast simulation of the detector response is a vital task in high-energy physics (HEP). Traditional Monte-Carlo methods form the backbone of modern particle physics simulation software but are computationally expensive. We present a machine-learning-based approach to fast simulation of the Focusing Aerogel Ring Imaging Cherenkov (FARICH) detector response. Given a particle track and momentum, ...
Added: May 19, 2026