Все выпуски

В данной работе представлен новый подход к интерпретации логических формул для синтеза алгоритмов и программ. Предложенный метод сочетает в себе черты реализации Клини и интерпретации Гёделя «диалектика», но не опирается на них непосредственно. Рассматривается простой вариант позитивного языка логики предикатов без функций, с конъюнкцией, дизъюнкцией, импликацией и кванторами всеобщности и существования. Описана новая реализационная семантика формул и секвенций, в которой рассматривается не просто реализация формулы, а реализация с дополнительной поддержкой. Реализация примерно соответствует реализации Клини. Поддержка предоставляет дополнительные данные в пользу того, что реализация корректна. Поддержка должна подтвердить, что реализация работает корректно для формулы в любых корректных условиях применения. Представлен язык доказательств, для которого доказана теорема о корректности, показывающая, что любая выводимая секвенция имеет реализацию и поддержку, подтверждающую, что эта реализация работает правильно для этой формулы в любых корректных условиях при подходящем интерпретаторе используемых программ.

This paper presents a novel approach to interpreting logical formulas for synthesizing algorithms and programs. The proposed method combines features of Kleene realizability and Gödel's “dialectica” interpretation but does not rely on them directly. A simple version of positive predicate logic without functions is considered, including conjunction, disjunction, implication, and universal and existential quantifiers. A new realizability semantics for formulas and sequents is described, which considers not just a realization of a formula, but a realization with additional support. The realization roughly corresponds to Kleene realizability. The support provides additional data in favor of the correctness of the realization. The support must confirm that the realization works correctly for the formula under any valid conditions of application. A proof language is presented for which a correctness theorem is proved showing that any derivable sequent has a realization and support confirming that this realization works correctly for this formula under any valid conditions with a suitable interpreter for the programs used.

Работа посвящена построению приближенных решений краевых задач в прямоугольнике для нагруженного модифицированного уравнения влагопереноса дробного порядка с оператором Бесселя, выступающих в качестве математических моделей движения влаги и солей в почвах с фрактальной организацией. Построены разностные схемы для дифференциальных задач. Методом энергетических неравенств выведены априорные оценки решений рассматриваемых задач в дифференциальной и разностной трактовках. Из полученных априорных оценок следуют единственность, устойчивость решения по начальным данным и правой части, а также сходимость решения разностной задачи к решению соответствующей дифференциальной задачи со скоростью, равной порядку погрешности аппроксимации. Построен алгоритм численного решения разностных схем, полученных при аппроксимации краевых задач для нагруженного модифицированного уравнения влагопереноса дробного порядка с оператором Бесселя. Проведены численные эксперименты, иллюстрирующие полученные в работе теоретические выкладки.

The paper is devoted to the construction of approximate solutions of boundary value problems in a rectangle for a loaded modified fractional-order moisture transfer equation with the Bessel operator, which act as mathematical models of the movement of moisture and salts in soils with fractal organization. Difference schemes for differential problems are constructed. The method of energy inequalities is used to derive a priori estimates of solutions to the problems under consideration in differential and difference interpretations. The obtained a priori estimates are followed by uniqueness, stability of the solution from the initial data and the right part, as well as convergence of the solution of the difference problem to the solution of the corresponding differential problem with a speed equal to the order of approximation error. An algorithm for the numerical solution of difference schemes obtained by approximating boundary value problems for a loaded modified fractional-order moisture transfer equation with the Bessel operator is constructed.

В представленной работе описывается способ проектирования языка подстановок для генерации электронных документов на основе содержимого баз данных и файлов. Проектируемый язык предполагает возможность работы как с одной базой данных, так и с большим числом однотипных баз, имеет модульную структуру, при которой для сложных элементов документа используются шаблоны на отдельных вспомогательных языках. Один из таких вспомогательных языков - язык для генерации таблиц, имеющих сложную структуру с вложенными подтаблицами и расширенными ячейками. Описываемый язык позволяет группировать в удобном для чтения виде большие объемы разнообразных данных. Также предполагается, что язык подстановок и его вспомогательные конструкции не будут привязаны к каким-либо форматам входных и выходных данных, что позволяет использовать любые подходящие форматы путем написания соответствующего модуля для интерпретатора.

This paper describes an approach to designing a substitution language for generating electronic documents based on the contents of databases and files. The proposed language involves the ability to work both with a single database and with a large number of databases with a similar structure. It has a modular structure, where additional auxiliary languages are used for generating complex document elements. One such auxiliary language is the language for generation of tables having a complex structure with subtables and extended cells. This auxiliary language will make it possible to group in a readable form a large amount of various data. It is also assumed that the substitution language and its auxiliary languages will not be bound to any input or output data formats, which will allow using any suitable formats by writing an appropriate module for the interpreter.

Обсуждается проблема корректного использования программных пакетов, в которых реализованы методы решения некорректных задач. К некорректным задачам относится большинство задач обработки экспериментальных данных. При использовании методов решения некорректных задач существует проблема неединственности решения, которая решается путем введения априорной информации. Получение априорной информации возможно разными способами, но количественные оценки предполагают использование дополнительных методов анализа данных. Очевидно, что дополнительные методы не должны быть сложнее и трудозатратнее основного метода обработки данных. На примере использования программы анализа данных электроразведки RES3DINV продемонстрирована роль априорной информации для получения достоверных результатов. Программный пакет RES3DINV применяется для построения модели грунта по измеренным значениям удельного сопротивления методами электроразведки. При использовании реализованного в программном пакете метода инверсии необходимо задавать входные параметры, характеризующие геометрические размеры объекта аномального сопротивления, которые априори, как правило, неизвестны. На модельных объектах продемонстрировано как влияет некорректное задание входных параметров на результат интерпретации данных. Показано, что в качестве способа получения априорной информации можно использовать метод векторного анализа. Этот метод позволяет получать оценки геометрических параметров аномального объекта и не требует больших временных и ресурсных затрат, и может быть использован непосредственно на месте полевых экспериментальных измерений.

We discuss the problem of proper use of software packages that implement methods for solving ill-posed problems. Most of the problems of processing experimental data belong to ill-posed problems. When using methods for solving ill-posed problems, there is a problem of non-uniqueness of the solution, which is solved by introducing a priori information. Obtaining a priori information is possible in different ways, but quantitative estimates involve the use of additional methods for data analysis. Obviously, additional methods should not be more complicated and labor intensive than the main data processing method. Using the RES3DINV electrical prospecting data analysis software as an example, the role of a priori information for obtaining reliable results is demonstrated. The RES3DINV software is used to build a soil model from the measured values of resistivity using electrical survey’s methods. When using the inversion method implemented in the software package, it is necessary to set the input parameters describing the geometric dimensions of the anomalous resistance object, which are usually unknown a priori. By model objects we demonstrate how the incorrect setting of input parameters affects the result of data interpretation. We show that the vector analysis method can be used as a way to obtain a priori information. This method allows us to obtain estimates of the geometric parameters of an anomalous object, does not involve high time and resource expenses, and can be used directly at the site of field experimental measurements.