Browse

You are looking at 1 - 10 of 621 items for :

  • Artificial Intelligence x
Clear All
Open access

Amira Mohamed, Shady S. Refaat and Haitham Abu-Rub

Abstract

Smart grid (SG) is the solution to solve existing problems of energy security from generation to utilization. Examples of such problems are disruptions in the electric grid and disturbances in the transmission. SG is a premium source of Big Data. The data should be processed to reveal hidden patterns and secret correlations to extrapolate the needed values. Such useful information obtained by the so-called data analytics is an essential element for energy management and control decision towards improving energy security, efficiency, and decreasing costs of energy use. For that reason, different techniques have been developed to process Big Data. This paper presents an overview of these techniques and discusses their advantages and challenges. The contribution of this paper is building a recommender system using different techniques to overcome the most obstacles encountering the Big Data processes in SG. The proposed system achieves the goals of the future SG by (i) analyzing data and executing values as accurately as possible, (ii) helping in decision-making to improve the efficiency of the grid, (iii) reducing cost and time, (iv) managing operating parameters, (v) allowing predicting and preventing equipment failures, and (vi) increasing customer satisfaction. Big Data process enables benefits that were never achieved for the SG application.

Open access

Grzegorz Iwański, Paweł Maciejewski and Tomasz Łuszczyk

Abstract

The paper presents a control method for the three-phase power converter operating under unbalanced grid voltage conditions. The method uses a new transformation to the non-Cartesian frame, which makes the controlled current vector components balanced in this frame even if originally the three-phase current is referenced as unbalanced. Furthermore, Park’s transformation makes the controlled variables constant, which allows to apply proportional–integral terms as current controllers independent of the required control target. Several control targets known from literature have been analyzed with regard to the required new transformation parameters, and the transformation parameters for all targets have been found. Simulation results are shown to prove the theoretical analysis, and the experimental test results are presented as practical validation of the proposed use of the non-Cartesian frame in control.

Open access

Grzegorz Iwański, Paweł Maciejewski and Tomasz Łuszczyk

Abstract

One of the currently investigated problems in power electronics-based electrical energy conversion is proper operation of electronic converters during grid voltage imbalance and harmonics. In classic control methods, it introduces oscillations of variables, resulting in the necessity to improve control systems with signals filtration and usually by application of resonant terms as part of current controllers. The paper presents a new approach to grid-connected inverter control based on transformation to a non-Cartesian frame, the parameters of which are correlated with grid voltage asymmetry. The proposed method results in resignation from resonant terms used as controllers and their replacement with proportional–integral terms for which anti-wind-up structures are significantly simpler than for oscillatory terms. The paper presents new transformation principles, features and some simulation results showing the waveforms of signals transformed to the new non-Cartesian frame.

Open access

Roberto Eduardo Quintal-Palomo

Abstract

This manuscript analyzes the operation of an interior permanent magnet (IPM) machine working as a permanent magnet synchronous generator (PMSG). The partial demagnetization operation is analyzed. To obtain more accurate voltages and currents of the machine, finite element analysis (FEA) is used in co-simulation with the full converter and the converter’s control algorithm. Direct field oriented control (DFOC) shows robustness by maintaining the speed even with a 25% demagnetized PMSG. Also, an analysis of the rotating reference frame DQ signals is done to asses demagnetization.

Open access

Adrian Jaszczak

Summary

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:

i := val.1 j := val.2 b := val.3 n := val.4 s := val.5 while (i <> n) i := i + j s := s * b return s

computing the natural n power of given complex number b, where variables i, b, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = b, loc/.4 = n and loc/.5 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [17]).

The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [14],[16],[7],[5].

Open access

Adrian Jaszczak and Artur Korniłowicz

Summary

In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:

i := val.1 j := val.2 n := val.3 s := val.4 while (i <> n) i := i + j s := s * i return s

computing the factorial of given natural number n, where variables i, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = n and loc/.4 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [16]).

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [13],[15],[7],[5].

Open access

Christoph Schwarzweller

Summary

This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial pF [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [9], [4], [6].

In this first part we show that an irreducible polynomial pF [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ: FF [X]/<p> and show that the translated polynomial ϕ(p) has a root over F [X]/<p>.

Because F is not a subfield of F [X]/<p> we construct in the second part the field (E \ ϕF )∪F for a given monomorphism ϕ : FE and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that F ∩ E =∅, in particular Kronecker’s construction can be formalized for fields F with F \ F [X] =∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F of F with F′F′ [X] ∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈[X] = ∅and 𝕉 ∩ 𝕉[X] = ∅, respectively.

In the fourth part we finally define field extensions: E is a field extension of F i F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ : FF [X]/<p>. Together with the first part this gives - for fields F with FF [X] = ∅ - a field extension E of F in which pF [X]\F has a root.

Open access

Christoph Schwarzweller

Summary

This is the second part of a four-article series containing a Mizar [2], [1] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial pF [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [5], [3], [4].

In the first part we show that an irreducible polynomial pF [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ : F → F [X]/<p> and show that the translated polynomial ϕ (p) has a root over F [X]/<p>.

Because F is not a subfield of F [X]/<p> we construct in this second part the field (E \ ϕF )∪F for a given monomorphism ϕ : F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that FE = ∅, in particular Kronecker’s construction can be formalized for fields F with FF [X] = ∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F′ of F with F′F′ [X] ∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈 [X] = ∅ and 𝕉 ∩ 𝕉 [X] = ∅, respectively.

In the fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have FE as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ : F → F [X]/<p>. Together with the first part this gives - for fields F with F ∩ F [X] = ∅ - a field extension E of F in which pF [X]\F has a root.

Open access

Sebastian Koch

Summary

In [3] the existence of the Cantor normal form of ordinals was proven in the Mizar system [6]. In this article its uniqueness is proven and then used to formalize the natural sum of ordinals.

Open access

Kazuhisa Nakasho

Summary

In this article, using the Mizar system [5], [2], the isomorphisms from the space of multilinear operators are discussed. In the first chapter, two isomorphisms are formalized. The former isomorphism shows the correspondence between the space of multilinear operators and the space of bilinear operators.

The latter shows the correspondence between the space of multilinear operators and the space of the composition of linear operators. In the last chapter, the above isomorphisms are extended to isometric mappings between the normed spaces. We referred to [6], [11], [9], [3], [10] in this formalization.