Die m-Grade logischer Entscheidungsprobleme.
In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against...
In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].
In this article, we describe the differential equations on functions from R into real Banach space. The descriptions are based on the article [20]. As preliminary to the proof of these theorems, we proved some properties of differentiable functions on real normed space. For the proof we referred to descriptions and theorems in the article [21] and the article [32]. And applying the theorems of Riemann integral introduced in the article [22], we proved the ordinary differential equations on real...
In this article we formalized the Fréchet differentiation. It is defined as a generalization of the differentiation of a real-valued function of a single real variable to more general functions whose domain and range are subsets of normed spaces [14].
This paper is the first in a sequence on the structure of sets of solutions to systems of equations in a free group, projections of such sets, and the structure of elementary sets defined over a free group. In the first paper we present the (canonical) Makanin-Razborov diagram that encodes the set of solutions of a system of equations. We continue by studying parametric families of sets of solutions, and associate with such a family a canonical graded Makanin-Razborov diagram, that encodes the collection...
We prove that the positive-existential theory of addition and divisibility in a ring of polynomials in two variables A[t₁,t₂] over an integral domain A is undecidable and that the universal-existential theory of A[t₁] is undecidable.
The theory of discriminator algebras and varieties has been investigated extensively, and provides us with a wealth of information and techniques applicable to specific examples of such algebras and varieties. Here we give several such examples for Boolean algebras with a residuated binary operator, abbreviated as r-algebras. More specifically, we show that all finite r-algebras, all integral r-algebras, all unital r-algebras with finitely many elements below the unit, and all commutative residuated...
The paper deals with binary operations in the unit interval. We investigate connections between families of triangular norms, triangular conorms, uninorms and some decreasing functions. It is well known, that every uninorm is build by using some triangular norm and some triangular conorm. If we assume, that uninorm fulfils additional assumptions, then this triangular norm and this triangular conorm have to be ordinal sums. The intervals in ordinal sum are depending on the set of values of a decreasing...
We present an elementary proof (purely in equational logic) that distributive groupoids are symmetric-by-medial.
In 2015, a new class of fuzzy implications, called ordinal sum implications, was proposed by Su et al. They then discussed the distributivity of such ordinal sum implications with respect to t-norms and t-conorms. In this paper, we continue the study of distributivity of such ordinal sum implications over two newly-born classes of aggregation operators, namely overlap and grouping functions, respectively. The main results of this paper are characterizations of the overlap and/or grouping function...