Computer-Assisted Proofs and Symbolic Computations

We discuss some main points of computer-assisted proofs based on reliable numerical computations. Such so-called self-validating numerical methods in combination with exact symbolic manipulations result in very powerful mathematical software tools. These tools allow proving mathematical statements (existence of a fixed point, of a solution of an ODE, of a zero of a continuous function, of a global minimum within a given range, etc.) using a digital computer. To validate the assertions of the underlying theorems fast finite precision arithmetic is used. The results are absolutely rigorous. To demonstrate the power of reliable symbolic-numeric computations we investigate in some details the verification of very long periodic orbits of chaotic dynamical systems. The verification is done directly in Maple, e.g. using the Maple Power Tool intpakX or, more efficiently, using the C++ class library C-XSC.

Essential Arity Gap of Boolean Functions

In this paper we investigate the Boolean functions with maximum essential arity gap. Additionally we propose a simpler proof of an important theorem proved by M. Couceiro and E. Lehtonen in [3]. They use Zhegalkin’s polynomials as normal forms for Boolean functions and describe the functions with essential arity gap equals 2. We use to instead Full Conjunctive Normal Forms of these polynomials which allows us to simplify the proofs and to obtain several combinatorial results concerning the Boolean functions with a given arity gap. The Full Conjunctive Normal Forms are also sum of conjunctions, in which all variables occur.

A Note on Totally Bounded Quasi-Uniformities

We present the original proof, based on the Doitchinov completion, that a totally bounded quiet quasi-uniformity is a uniformity. The proof was obtained about ten years ago, but never published. In the mean-time several stronger results have been obtained by more direct arguments [8, 9, 10]. In particular it follows from Künzi’s [8] proofs that each totally bounded locally quiet quasi-uniform space is uniform, and recently Déak [10] observed that even each totally bounded Cauchy quasi-uniformity is a uniformity.

Regular and Other Kinds of Extensions of Topological Spaces

∗ This work was partially supported by the National Foundation for Scientific Researches at the Bulgarian Ministry of Education and Science under contract no. MM-427/94.

Polynomial Expansions for Solutions of Higher-Order Bessel Heat Equation in Quantum Calculus

Mathematics Subject Class.: 33C10,33D60,26D15,33D05,33D15,33D90

Theorems on the Convergence of Series in Generalized Lommel-Wright Functions

Mathematics Subject Classification: 30B10, 30B30; 33C10, 33C20

The Initial Stage of Teaching Proof in Mathematics Course

This article discusses techniques for organization of propaedeutic stage of teaching proof in mathematics course. It identifies types of tasks that allow students of 5–6 classes to form the ability to carry out simple proofs. This article describes each type of tasks features, it gives some examples.

Well-Posedness of Diffusion-Wave Problem with Arbitrary Finite Number of Time Fractional Derivatives in Sobolev Spaces H^s

Mathematics Subject Classification 2010: 26A33, 33E12, 35S10, 45K05.

Series in Mittag-Leffler Functions: Inequalities and Convergent Theorems

MSC 2010: 30A10, 30B10, 30B30, 30B50, 30D15, 33E12

Generalized Fractional Calculus, Special Functions and Integral Transforms: What is the Relation?

Виржиния С. Кирякова - В този обзор илюстрираме накратко наши приноси към обобщенията на дробното смятане (анализ) като теория на операторите за интегриране и диференциране от произволен (дробен) ред, на класическите специални функции и на интегралните трансформации от лапласов тип. Показано е, че тези три области на анализа са тясно свързани и взаимно индуцират своето възникване и по-нататъшно развитие. За конкретните твърдения, доказателства и примери, вж. Литературата.

Fraction Space Revisited

Бойко Бл. Банчев - Знае се, че рационалните числа образуват интересни и богати на изчислителни възможности структури като редици на Фарей (Феъри) и безкрайни дървета. Малко внимание се обръща на по-общо, систематично излагане на основните свойства на дробите като множество. Понятия биват въвеждани без обосноваване, някои доказателства са ненужно изкуствени, а почти винаги и едните, и другите като че биват отнесени към една или друга особена структура, вместо към множеството на дробите изобщо. Изненадващо е, че някои същностни твърдения изглежда дори не са формулирани в литературата по теория на числата. Тази статия има за цел да подобри състоянието на нещата в това отношение, като предлага общо, подходящо подредено изложение на понятия и свързани с тях твърдения. Като допълнение са представени бележки върху пораждането на множеството от всички дроби – откритие значително по-старо, отколкото е прието да се смята.

Verification of Procedural Programs via Building their Generalized Nets Models

Магдалина Василева Тодорова - В статията е описан подход за верификация на процедурни програми чрез изграждане на техни модели, дефинирани чрез обобщени мрежи. Подходът интегрира концепцията “design by contract” с подходи за верификация от тип доказателство на теореми и проверка на съгласуваност на модели. За целта разделно се верифицират функциите, които изграждат програмата относно спецификации според предназначението им. Изгражда се обобщен мрежов модел, специфициащ връзките между функциите във вид на коректни редици от извиквания. За главната функция на програмата се построява обобщен мрежов модел и се проверява дали той съответства на мрежовия модел на връзките между функциите на програмата. Всяка от функциите на програмата, която използва други функции се верифицира и относно спецификацията, зададена чрез мрежовия модел на връзките между функциите на програмата.

Control Systems with Constraints and Uncertain Initial Conditions

AMS subject classification: 49N55, 93B52, 93C15, 93C10, 26E25.

On the logarithm of the differential operator

Two different proofs are given of the fact that In s= — s {In t + C}, where С is Euler’s constant.

On Optimal Quadratic Lagrange Interpolation: Extremal Node Systems with Minimal Lebesgue Constant via Symbolic Computation

ACM Computing Classification System (1998): G.1.1, G.1.2.