A sequent calculus S for the variety tqBa of all topological quasi-Boolean algebras is established. Using a construction of syntactic finite algebraic model, the finite model property of S is shown, and thus the decidability of S is obtained. We also introduce two non-distributive variants of topological quasi-Boolean algebras. For the variety TDM5 of all topological De Morgan lattices with the axiom 5, we establish a sequent calculus S5 and prove that the cut elimination holds for it. Consequently the decidability (...) of S5 is established. Furthermore, this proof-theoretic method is applied to some subvarieties of TDM5. (shrink)

As a promising method with excellent characteristics in terms of resilience and dependability, distributed methods are gradually used in the field of energy management of microgrid. However, these methods have more stringent requirements on the working conditions, which will make the system more sensitive to communication failures and cyberattacks. As a result, it is both theoretical merits and practical values to investigate the malicious effect of cyber attacks on microgrid. This paper studies the distributed economic dispatch problem under denial-of-service attacks (...) for the microgrid, in which each generator can communicate with its neighbors and has the computational capability to implement local operation. Firstly, a DoS attack model is proposed, in which the DoS attacker intentionally jams the communication channel to deteriorate the performance of the microgrid. Then, the evolution mechanism of the dispatch system of the microgrid under different attack scenarios is adequately discussed. On this basis, an optimal attack strategy based on enumerating-search algorithm is presented to allocate the limited attack resources reasonably, so as to maximize the effect of DoS attacks. Finally, the validity of the theoretical studies about the attack effect under different scenarios and the effectiveness of the proposed enumerating-search-based optimal attack strategy are illustrated through the simulation examples on the IEEE 57-bus system and IEEE 39-bus system, respectively. (shrink)