PROBLEMS IN PROGRAMMING
Not a member yet
761 research outputs found
Sort by
Математичні методи планування в системах, що складаються з раціональних агентів
Get PDFThe paper is devoted to mathematical methods of planning in systems consisting of rational agents. An agent is an autonomous object that has sources of information about the environment and influences this environment. A rational agent is an agent who has a goal and uses optimal behavioral strategies to achieve it. It is assumed that there is a utility function, which is defined on the set of possible sequences of actions of the agent and takes values in the set of real numbers. A rational agent acts to maximize the utility function. If rational agents form a system, then they have a common goal and act in an optimal way to achieve it. Agents use the optimal solution of the extreme problem, which corresponds to the goal of the system. The problem of linear programming is considered, in which the number of product sets produced by the system is maximized. To solve the nonlinear problem of optimizing the production plan, the conditional gradient method is used, which at each iteration allows a posteriori estimation of the error of the solution and allows stopping the calculation process after reaching the required accuracy. Since the rational agents that are part of the system can have separate optimality criteria, multi-criteria optimization problems appear. The article considers a humanmachine procedure for solving such problems, which is connected with the conditional gradient method and uses information from the decision-maker (DM) at each iteration. The difficulties of this approach are that the DM is not able to make decisions many times under the condition of a significant number of iterations of the nonlinear programming method. The article proposes to replace OPR with an artificial neural network. Nonlinear and stochastic programming methods are used to find optimal parameters of this network.Prombles in programming 2024; 2-3: 231-238Робота присвячена математичним методам планування в системах, що складаються з раціональних агентів. Агентом вважається автономний об’єкт, який має джерела інформації про навколишнє середовище та впливає на це середовище. Раціональним агентом вважається агент, який має мету і заради її досягнення використовує оптимальні стратегії поведінки. Вважається, що існує функція корисності, яка визначена на множині можливих послідовностей дій агента і приймає значення в множині дійсних чисел. Раціональний агент діє так, щоб максимізувати функцію корисності. Якщо раціональні агенти утворюють систему, то вони мають спільну мету і діють оптимальним способом для її досягнення. Агенти використовують оптимальний розв’язок екстремальної задачі, який відповідає меті системи. Розглянуто задачу лінійного програмування, в якій максимізується кількість виготовлених системою комплектів продукції. Для розв’язування нелінійної задачі оптимізації плану виготовлення продукції застосовується метод умовного градієнта, який на кожній ітерації допускає апостеріорну оцінку похибки ортиманого розв’язку та дозволяє зупинити процес обчислень після досягнення потрібної точності. Оскільки раціональні агенти, що входять до складу системи, можуть мати окремі критерії оптимальності, виникають задачі багатокритеріальної оптимізації. В статті розглядається людино-машинна процедура розв’язування таких задач, яка пов’язана з методом умовного градієнта і на кожній ітерації використовує інформацію від особи, що приймає рішення (ОПР). Труднощі такого підходу полягають у тому, що ОПР не в змозі багаторазово приймати рішення за умови значної кількості ітерацій метода нелінійного програмування. В статті запропоновано замінити ОПР штучною нейронною мережею. Для пошуку оптимальних значень параметрів цієї мережі застосовуються методи нелінійного та стохастичного програмування.Prombles in programming 2024; 2-3: 231-23
Формальна верифікація нейронних мереж глибокого навчання
Get PDFThis paper introduces a method for the formal verification of neural networks using a Satisfiability Modulo Theories (SMT) solver. This approach enables the mathematical validation of specific neural network properties, enhancing their predictability. We propose a method for simplifying a neural network’s computational graph within certain input space regions. This is achieved by replacing neurons’ piecewise-linear activation functions with a subset of their linear segments. This optimization hypothesizes a simpler interpretation of a neural network over limited input data ranges. The simplified interpretation is derived from the incremental simplification of the neural network graph, achieved by solving local SMT tasks on a neuron-by-neuron basis. This optimization significantly speeds up the verification algorithm compared to solving a single SMT task over the entire unoptimized network graph. The method is applicable to any deep neural networks with piecewise-linear activation functions. The approach’s effectiveness was demonstrated by automatically verifying a network traffic classifier specializing in botnet activity detection. The classification model was tested for robustness against adversarial attacks, where attackers attempt to evade detection by introducing specially crafted disturbances into the network data. The verification procedure was conducted over regions in the feature-space near the classifier’s decision boundary. The results contribute to the prospects for more active application of artificial intelligence models in cybersecurity, where result predictability and interpretability are crucial. Additionally, the neuron - wise simplification technique proposed is a promising direction for further development in neural network verification.Prombles in programming 2024; 2-3: 253-262У цій роботі представлено спосіб формальної верифікації властивостей нейронних мереж за допомогою "Satisfiability Modulo Theories" (SMT) розв’язувача. Цей підхід дозволяє математично доводити специфічні властивості нейромереж, що робить їх більш передбачуваними. У процесі дослідження було розроблено новий метод спрощення обчислювального графа нейромережі над певними регіонами вхідного простору, шляхом заміни кусково-лінійних функцій активації нейронів на підмножину їхніх лінійних сегментів. Запропонований спосіб оптимізації ґрунтується на гіпотезі існування значно простішої інтерпретації нейромережі на обмежених діапазонах вхідних даних. У роботі пропонується спосіб отримання такої спрощеної інтерпретації через понейронне розв’язування локальних SMT-задач з інкрементальним спрощенням графу нейромережі. Ця оптимізація дозволила значно прискорити алгоритм верифікації порівняно з розв’язанням єдиної SMT-задачі над суцільним неоптимізованим графом мережі. Описаний метод можна застосовувати для верифікації довільних повнозв’язних нейромереж глибокого навчання з кусково-лінійними функціями активації. Для практичної демонстрації результатів створений метод верифікації було застосовано для перевірки роботи нейромережі-аналізатора мережевого трафіку, метою якого є виявлення активності ботнетів. Модель класифікації перевірялась на стійкість до «змагальних атак» – спроб зловмисника уникнути виявлення, вносячи спеціальні збурення в дані, що класифікуються. В роботі було проведено автоматизовану перевірку коректності роботи класифікатора над сумнівними регіонами даних, які розміщені біля межі ухвалення рішень. Отримані результати роблять важливий внесок у розвиток застосування штучного інтелекту в царині кібербезпеки, де інтерпретація та передбачуваність є критично необхідними. Крім того, запропонований метод понейронного спрощення є перспективним напрямком для подальшого розвитку верифікації нейронних мереж.Prombles in programming 2024; 2-3: 253-26
Представлення монадичних ефектів у немонадичній формі
Get PDFModern programming relies heavily on effects systems. In the context of the development of programming languages, two approaches to understanding effects are distinguished: the first recognizes an effect as a characteristic of a program that affects the execution environment, separating it from a simple calculation (that is, effects are not taken into account in the system of language types, which is typical for imperative programming languages); the second considers an effect as an aspect of program interpretation that affects the process of its interpretation (such effects are considered in the type system as higher-order types, and this approach is characteristic of functional programming). In industrial programming, the first approach is preferred because of its efficiency in rapid development and less complex concepts. However, this leads to the loss of the possibility of automatic analysis of effects using type systems and increases the difficulty of finding errors. Monads are a convenient tool for describing effects because they have a built-in computation composition operation and can sink values into the monadic environment. A direct contextual representation of effects can be useful for application developers because it reduces cognitive load from syntactic noise while preserving information about effects in data types. This representation also allows for cross-platform applications that can use both monadic and non-monadic effect systems. The paper describes the ergonomic programming language interface for working with monadic effects, which encapsulates the logic of computation and associated non-computational operations in the effect system monad, and describes the direct context encoding technique. The translation of the direct context encoding into the monadic form is implemented in the form of a Scala compiler plugin, which is available as an open source. The use of conditional effects compilation to organize cross-platform interfaces that combine different methods of implementing effects on different platforms is also discussed.Prombles in programming 2024; 2-3: 116-123 Сучасне програмування значною мірою покладається на системи ефектів. У контексті розробки мов програмування виокремлюються два підходи до розуміння ефектів: перший визнає ефект як характеристику програми, яка впливає на середовище виконання, відокремлюючи її від простого обчислення (тобто ефекти не враховуються в системі типів мови, що є типовим для імперативних мов програмування); другий розглядає ефект як аспект інтерпретації програми, який впливає на процес її інтерпретації (такі ефекти враховуються в системі типів як типи вищого порядку, і цей підхід характерний для функціонального програмування). В індустріальному програмуванні перевагу надають першому підходу через його ефективність у швидкій розробці та меншій складності концепцій. Проте це призводить до втрати можливості автоматичного аналізу ефектів за допомогою систем типів та збільшує складність знаходження помилок. Монади є зручним інструментом для опису ефектів, оскільки вони мають вбудовану операцію композиції обчислень і можуть занурювати значення у монадичне середовище. Пряме контекстне представлення ефектів може бути корисним для розробників програм, оскільки це дозволяє знизити когнітивне навантаження від синтаксичного шуму і водночас зберігає інформацію про ефекти у типах даних. Таке представлення також дозволяє створювати кросплатформові програми, які можуть використовувати як монадичні, так і немонадичні системи ефектів. У статті розглядається проблематика створення ергономічного інтерфейсу для роботи з монадичними ефектами, які включають логіку обчислень та пов’язані операції у монаді системи ефектів, а також описується пряме контекстне представлення ефектів. Перетворення прямого контекстного представлення на монадичну форму реалізовано через плагін компілятора Scala, що доступний у вигляді відкритого коду. Також розглядається використання умовної компіляції ефектів для створення крос-платформових інтерфейсів, що об’єднують різні методи реалізації ефектів на різних платформах.Prombles in programming 2024; 2-3: 116-123
Комп’ютерна модель трансформації організації
Get PDFThe article is devoted to the topical issue of creating a computer system to support management decisions regarding the optimization of the transformation processes of organizations when adapting to the conditions of the implementation of new projects. The purpose of the article is to increase the efficiency of large organizational structures by creating computer models that, on the one hand, have a sufficient level of adequacy, and on the other hand, have a visual interpretation of the main input parameters, which allows them to be easily determined on the basis of empirical data. A computer model in the form of a simulation model is considered as the basis of the management decision support system. In the work, the analysis of existing studies is performed, the relevance of the problem is substantiated. The analysis of existing exponential and linear models was performed. Reasoned adequacy of logistic models. The differential form of logistic models is considered. The ordinary differential equation of the logistic model is solved in order to obtain the integral form of the logistic equation. The parameters of the computer model are introduced, which are easy to determine numerically on the basis of empirical data. A mathematical model of the beneficial effect of the organization in the conditions of transformation was created, which establishes the dependence of the beneficial effect on the input resource (time). The model is created as a combination of several logistic dependencies, each of which is responsible for increasing or decreasing the beneficial effect. The model takes into account the dependences of the growth of the useful effect for the main and new technologies, the decrease of the useful effect as a result of the moral obsolescence of the technology, and the gradual decrease of the useful effect due to the directive shutdown of the old technology. The structure of the model allows its scaling to more complex development scenarios. The concept of the degree of insensitivity of the useful effect to small amounts of input resources at the initial stages of the organization's development is introduced. The dependence of the initial result on the degree of insensitivity was studied. The model was implemented using the MatLab algorithmic language.Prombles in programming 2024; 2-3: 84-91 Стаття присвячена актуальному питанню створення комп’ютерної системи підтримки управлінських рішень щодо оптимізації процесів трансформації організацій при адаптації під умови виконання нових проєктів. Метою статті є підвищення ефективності діяльності великих організаційних структур за рахунок створення комп’ютерних моделей, які з одного боку мають достатній рівень адекватності, а з іншого - мають наочну інтерпретацію основних вхідних параметрів, що дозволяє легко їх визначати на основі емпіричних даних. За основу системи підтримки управлінських рішень розглядається комп’ютерна модель у вигляді імітаційної моделі. В роботі виконаний аналіз існуючих досліджень, обґрунтована актуальність задачі. Виконаний аналіз існуючих експоненціальних та лінійних моделей. Обґрунтована адекватність логістичних моделей. Розглянута диференціальна форма логістичних моделей. Звичайне диференціальне рівняння логістичної моделі розв’язане з метою отримання інтегральної форми логістичного рівняння. Введені параметри комп’ютерної моделі, які легко визначати чисельно на основі емпіричних даних. Створена математична модель корисного ефекту організації в умовах трансформації, яка встановлює залежність корисного ефекту від вхідного ресурсу (часу). Модель створена у вигляді комбінації декількох логістичних залежностей, кожна з яких відповідає за зростання або за зменшення корисного ефекту. В моделі враховані залежності зростання корисного ефекту для основної та нової технологій, зниження корисного ефекту внаслідок морального старіння технології та поступове зниження корисного ефекту внаслідок директивного вимкнення старої технології. Структура моделі дозволяє її масштабування на більш складні сценарії розвитку. Введене поняття ступеня нечутливості корисного ефекту до невеликих величин вхідних ресурсів на початкових етапах розвитку організації. Досліджена залежність вихідного результату від ступеня нечутливості. Модель реалізована алгоритмічною мовою MatLab.Prombles in programming 2024; 2-3: 84-9
Розробка методів сегментаці рослинності за висотою та оцінка їх ефективност і точності
Get PDFHeight-based vector vegetation segmentation is one of the critical aspects of spatial analysis. This segmented data is used in radio propagation modeling, environmental monitoring, and vegetation mapping. Many studies on vector vegetation segmentation focus on delineating individual tree crowns, allowing detailed data sets to be obtained. However, the high level of detail results in a substantial data volume, making it impractical to use these datasets over large areas, such as an entire country. Segmentation of large vector data sets remains a significant challenge in geospatial data creation. In our study, we developed three different segmentation methods: hexagon segmentation, convolution segmentation, and random points method. A test data fragment was processed to compare the proposed methods and accuracy and volume metrics were calculated.Prombles in programming 2024; 2-3: 313-318Cегментація векторної рослинності за висотою є одним із важливих етапів просторового аналізу. Цей тип даних використовується у побудові моделей розповсюдження радіосигналів, екологічному моніторингу та картографуванні рослинності. На сьогодні існує багато досліджень із сегментації векторної рослинності, що зосереджені на виокремленні індивідуальних крон дерев та дозволяють отримати деталізовані набори даних. Але наслідком високої деталізації є суттєвий обсяг, який унеможливлює використання цих даних на великих територіях, наприклад, в масштабі цілої країни. Сегментація великих масивів векторних даних досі є суттєвим викликом у сфері створення геопросторових даних. В процесі нашого дослідження ми розробили три різні методи сегментації: сегментація шестикутниками, сегментація за допомогою згорткових фільтрів та метод випадкових точок. Для порівняння запропонованих методів був опрацьований тестовий фрагмент даних та прораховані метрики точності та об’єму.Prombles in programming 2024; 2-3: 313-31
Метод пріоритезації вимог в програмній інженерії
No full textIn software development processes, requirements prioritization plays a key role. Proper gathering of requirements and their objective prioritization can ensure a sequential and effective development of a software project. With the increasing complexity of software, which is a characteristic of today, problems related to defining requirements also increase. It becomes increasingly challenging to identify the most important and essential requirements in a stream of wishes and recommendations, determining what should be the starting point of development and where the most attention should be focused. The task of requirements prioritization is multi-criterial and poses significant cognitive loads. Most researchers and professionals suggest expert methods for decision-making in such environments, which to some extent help solve the tasks at hand. However, among the known requirements prioritization methods, practically all involve qualitative descriptive analysis based on brainstorming techniques. At the same time, in the modern conditions of digitalization, providing decision support based on a comprehensive presentation of the information model of the subject area and processing through information technologies for quantitative assessment of alternatives is more promising. Another important capability of modern technologies is visualization of decision-making processes. Thus, this work explores a comprehensive prioritization method that involves a full presentation of the information picture of the subject area, including in the form of computer ontologies, applying a quantitative AHP method for comparing requirements, and visualized data in gra phs for considering alternatives. Additional use of a modified SWOT matrix allows for the disaggregation of requirements into their individual characteristics and consideration of their advantages for problem evaluation. The existence of such tools and the capabilities of information technologies confirm the effectiveness and stability of the proposed method.Problems in programming 2024; 2-3: 132-139У процесах розробки програмного забезпечення ключову роль відіграє пріоритезація вимог. Належне збирання вимог та їхня об’єктивна пріоритезація можуть забезпечити послідовний та ефективний розвиток програмного проєкту. Зі збільшенням складності програмного забезпечення, що є ознакою сьогодення, зростають і проблеми, пов’язані із визначенням вимог. Усе складнішим завданням стає виявлення в потоці побажань і рекомендацій найважливішого, найсуттєвішого, того, з чого треба починати розроблення і що варте найбільшої уваги. Задача ранжування вимог є багатокритеріальною і викликає значні когнітивні навантаження. Більшість із дослідників та фахівці пропонують для ухвалення рішень у такому середовищі експертні методи, які певною мірою дають змогу вирішувати поставлені задачі. Однак серед відомих методів пріоритезації вимог практично усі передбачають якісний описовий аналіз, що спирається на техніки інтелектуального штурму. В той же час в сучасних умовах цифровізації перспективнішим є забезпечення підтримки рішень на основі вичерпного подання інформаційної моделі предметної області та опрацювання за допомогою інформаційних технологій кількісних оцінок альтернатив. Також важливою можливістю сучасних технологій є забезпечення візуалізації процесів, пов’язаних із прийняттям рішень. Отже, у цій роботі досліджується комплексний метод пріоретизації, який передбачає вичерпне подання інформаційної картини предметної області, зокрема у вигляді комп’ютерних онтологій, застосування для порівняння вимог кількісного методу аналізу ієрархій та візуалізовані у графах дані щодо розгляду альтернатив. Додаткове використанням модифікованої матриці SWOT дозволяє проводити дезагрегування вимог до окремих їхніх характеристик та врахування переваг для оцінювання проблем. Наявність таких інструментів та можливостей інформаційних технологій підтверджують ефективність та стабільність запропонованого методу.Problems in programming 2024; 2-3: 132-13
Передавальне навчання для підвищення точності класифікації візуального трансформера на обмежених даних
Get PDFThis article examines the effectiveness of pre-training generative model based on a visual transformer and subsequent fine tuning for image classification tasks. The main problem of the study is the poor training efficiency of the visual transformer on a limited amount of data. It is possible to improve the accuracy of the image classification model by using transfer learning of the knowledge obtained during the previous training of the generative model on the same data. A subset of the standard Imagenet dataset - Tiny Imagenet was used to test the hypothesis. It contains 200 categories of around 500 images each. The size of each image is 64x64 pixels. For pre-training the generative model, patches are used to mask image segments. The training of restoring masked image pixels forces the model to pay attention to the context around the removed part, as well as to general visual patterns. This leads to a better understanding of visual information by the model as a whole and helps with further fine tuning of the model for the classification task. As a result of a series of experiments, it was possible to achieve an improvement in the accuracy of image classification from 40% to 44.7%, and an analysis of the effect of the overall degree of masking and patch size on it is given. Additionally, impact of different sizes of patches (2x2, 4x4, 8x8 pixels) and different percentages of masking (20/40/60 percent) of the input image were investigated in the paper.Prombles in programming 2024; 2-3: 247-252 У цій статті досліджується ефективність попереднього навчання генеративних моделей на основі візуального трансформера і подальшому навчанню моделі для задач класифікації зображень. Основною проблемою дослідження є погана ефективність навчання візуального трансформера на обмеженій кількості даних. Можна підвищити точність моделі класифікації зображень, використавши передавальне навчання знань, отриманих під час попереднього навчання генеративної моделі на тих самих даних. Для перевірки гіпотези була використана підмножина стандартного набору даних Imagenet, що містить 200 категорій по ~500 зображень. Розмір кожного зображення 64х64 пікселів. Для попереднього навчання генеративної моделі використовуються патчі для маскування сегментів зображення. Процес навчання відновлення замаскованих пікселів зображення змушує модель звертати увагу на контекст навколо видаленої частини, а також на загальні візуальні закономірності. Це приводить до кращого розуміння моделлю візуальної інформації в цілому і допомагає у подальшому навчанні моделі під задачу класифікації. В результаті серії експериментів вдалося досягти покращення точності класифікації зображень з 40% до 44.7%, а також наведено аналіз впливу на нього загального ступеню маскування та розмірності патчів. Додатково в роботі досліджені різні розмірності патчів (2x2, 4х4, 8х8 пікселів) й різний відсоток маскування (20/40/60 відсотків) вхідного зображення та вплив цих параметрів на передавальне навчання.Prombles in programming 2024; 2-3: 247-252
Програмування одновимірного та двовимірних токенів для токенізації земельних ділянок
No full textThe use of blockchain tools that allows spliting virtual objects into parts is considered. Examples of practical use of the developed algorithms are presented. The concept of one-dimensional and two-dimensional tokens representing one-dimensional and flat objects is proposed. Algorithms for the implementation of one-dimensional tokens are developed, and the peculiarities of their practical application are considered. A designed smart contract allows to conduct a basic list of operations with one-dimensional tokens. Algorithms, providing implementation of two-dimensional tokens, are proposed. Peculiarities of presenting territories of virtual worlds and land plots are suggested. A comparative analysis of the use of NFT and two-dimensional tokens for presenting the Earth surface areas is performed. Methods that ensure ownership of tokens at different levels are proposed.Prombles in programming 2024; 1: 38-47У публікації розглянуто ключові аспекти застосування блокчейн-інструментів, що дозволяють оперувати частинами віртуальних об’єктів. Для вирішення практичних задач пропонується використовувати одновимірні та двовимірні токени. Розроблено алгоритми та програмно реалізовано одновимірні токени на базі існуючих платформ смарт-контрактів. Запропоновані рішення дозволяють розділяти одновимірні об’єктів на частини та проводити транзакції із цими фрагментами. Розроблено алгоритми реалізації двовимірних токенів та розглянуті особливості їх застосування для представлення земельних ділянок та віртуальних територій. Визначено основні переваги двовимірних токенів у порівнянні із NFT при їх використанні для представлення ділянок земної поверхні. Розроблено алгоритми, що забезпечують володіння віртуальними об’єктами на різних рівнях.Prombles in programming 2024; 1: 38-4
Пошук максимальних незалежних множин вершин графа для вдосконалення програмних проєктів
Get PDFThe need is fixed to software project enhancing with seamless integration of technological-descriptive and normative project manage- ment approaches by means of classical Graph Discrete Optimization Problems tailoring for software project management tasks, poorly equipped with best practices within technological approach. Class of software project management tasks is proposed to demonstrate the benefits of such integration. Two Boolean linear programming problems are investigated for searching some maximum size indepen- dent set (Section 1) and an algorithm for searching all possible maximum size independent sets (Section 2). Section 3 presents Problem Statement for searching a given number of non-intersecting independent sets with maximum sum of vertices’ numbers within independent sets. Based on it, Vizing-Plesnevich algorithm is described for coloring the graph vertices with the minimum number of colors.To solve Boolean problems, both specialized mathematical programming language AMPL and corresponding solver program named gu- robi are used. For basic algorithms developed, reference AMPL code versions are given as well as their running results.Illustrative examples of software project enhancing with the algorithms elaborated are considered in Section 4, namely: 25 specialists being conflicted during their previous projects partitioning into coherent conflict-free sub-teams for software projects portfolio; schedule optimization for autonomous testing of reusable components within a critical software system; cores composing for independent teams in a critical software project.Prombles in programming 2022; 3-4: 73-84 Зафіксовано потребу вдосконалення програмного проекту за рахунок непротирічної інтеграції технологічно-описового та норма- тивного підходів проектного менеджменту шляхом налаштування класичних задач дискретної оптимізації на графах для задач керування програмним проектом, кращі практики розв’язання яких недостатньо регламентовані в руслі технологічного підходу. Запропоновано клас задач керування програмним проектом для демонстрації перспективності зазначеної інтеграції. Досліджено дві задачі булевого лінійного програмування для знаходження деякої незалежної множини максимального розміру (розділ 1) та алгоритм знаходження всіх можливих незалежних множин максимального розміру (розділ 2). У розділі 3 надано постановку задачі знаходження заданої кількості незалежних множин, які не перетинаються й мають найбільшу суму кількостей вершин у незалежних множинах. На її основі описано алгоритм Візинга-Плесневича для розфарбування вершин графа мінімальною кількістю кольорів. Для розв’язання булевих задач використано спеціалізовану мову математичного програмування AMPL і відповідну їй програму-солвер gurobi. Для основних розроблених алгоритмів наведено рамкові версії коду мовою AMPL та результати їх запускання.У розділі 4 розглянуто показові приклади вдосконалення програмного проекту за допомогою розроблених алгоритмів: формуван- ня з 25 фахівців, між якими в попередніх проектах мали місце конфлікти, згуртованих безконфліктних під-команд для портфеля програмних проектів; оптимізації розкладу автономного тестування компонентів повторного використання в складі критичної програмної системи; формування ядер незалежних команд у критичному програмному проекті.Prombles in programming 2022; 3-4: 73-8
Алгебраїчний підхід у аналізі юридичних документів
No full textIn this study, problems regarding the analysis of law articles and their conformance to legal documents are considered. The algebraic approach is used for the formal verification of legal texts that is presented as specification of behavior algebra. Having a formal presentation of legal texts allows for the application of algebraic methods, such as symbolic modeling, automatic proving of statements and algebraic matching. The approach was implemented for Ukrainian-language legal documents to detect inconsistency, incompleteness, and prove conformance. The analysis of legal texts has been implemented for Tax code and examples of inconsistency of some statements were demonstrated in the paper. Another experiment has been performed for checking of conformance of court statements, agreements, licenses, new laws, taxation acts to the articles of law with usage of methods of algebraic matching. The formalization of legal documents, like court verdicts, shall be implemented fully automatically, and the existing database with such documents shall provide the possibility to use big data technologies and machine learning. In this study, we consider the use of the algebraic approach in the analysis of legal requirements and law artifacts within the scope of the Insertion Modeling System (IMS). The subject of this research is the laws created by the legislature and the artifacts of legal activity, such as lawsuit decisions, agreements, licenses, and juridical cases. The problem to be considered is the analysis of legal documents for conformance with the law and the analysis of the law’s articles, checking for inconsisten- cies, incompleteness, and other interested properties. In this paper, we consider every element of the technology in detail, and we describe the methods and results of the experiments.Prombles in programming 2022; 3-4: 117-127У даному дослідженні розглядаються проблеми аналізу статей законодавства та їх відповідності правовим документам. Ми пропонуємо використання алгебраїчного підходу для формальної верифікації юридичних текстів, які представляються у ви- гляді специфікації алгебри поведінки. Наявність формального представлення юридичних текстів дозволяє застосовувати алге- браїчні методи, такі як символічне моделювання, автоматичне доведення тверджень і алгебраїчне зіставлення. Підхід реалізо- вано для україномовних правових документів для виявлення невідповідності, неповноти та підтвердження відповідності. Було здійснено аналіз законодавчих актів для Податкового кодексу і наведено приклади невідповідності деяких тверджень. Прове- дено ще один експеримент для перевірки відповідності судових актів, договорів, ліцензій, нових законів, актів про оподатку- вання статтям законодавства з використанням методів алгебраїчного зіставлення. Формалізація юридичних документів, таких як судові рішення, має здійснюватися повністю автоматично, а існуюча база даних із такими документами має забезпечувати можливість використання технологій big data та машинного навчання. У цьому дослідженні ми розглядаємо використання алгебраїчного підходу в аналізі законодавчих вимог і правових документів у межах системи інсерційного моделювання. Предметом дослідження є створені законодавчою владою закони та юридичні документи, такі як судові рішення, угоди, ліцензії та судові справи. Проблемою, яка розглядається, є аналіз нормативно-правових документів на відповідність закону та аналіз ста- тей закону, перевірка на невідповідності, неповноту та інші властивості. У цій роботі ми детально розглядаємо кожен елемент технології, описуємо методику та результати експериментів.Prombles in programming 2022; 3-4: 117-12