950 resultados para Gödel theorem
Resumo:
In this paper we use the Hermite-Biehler theorem to establish results on the design of proportional plus integral plus derivative (PID) controllers for a class of time delay systems. Using the property of interlacing at high frequencies of the class of systems considered and linear programming we obtain the set of all stabilizing PID controllers. As far as we know, previous results on the synthesis of PID controllers rely on the solution of transcendental equations. This paper also extends previous results on the synthesis of proportional controllers for a class of delay systems of retarded type to a larger class of delay systems. (C) 2009 Elsevier Ltd. All rights reserved.
Resumo:
This work deals with the nonlinear piezoelectric coupling in vibration-based energy harvesting, done by A. Triplett and D.D. Quinn in J. of Intelligent Material Syst. and Structures (2009). In that paper the first order nonlinear fundamental equation has a three dimensional state variable. Introducing both observable and control variables in such a way the controlled system became a SISO system, we can obtain as a corollary that for a particular choice of the observable variable it is possible to present an explicit functional relation between this variable one, and the variable representing the charge harvested. After-by observing that the structure in the Input-Output decomposition essentially changes depending on the relative degree changes, presenting bifurcation branches in its zero dynamics-we are able in to identify this type of bifurcation indicating its close relation with the Hartman - Grobman theorem telling about decomposition into stable and the unstable manifolds for hyperbolic points.
Resumo:
We present algorithms for computing the differential geometry properties of intersection Curves of three implicit surfaces in R(4), using the implicit function theorem and generalizing the method of X. Ye and T. Maekawa for 4-dimension. We derive t, n, b(1), b(2) vectors and curvatures (k(1), k(2), k(3)) for transversal intersections of the intersection problem. (C) 2008 Elsevier B.V. All rights reserved.
Resumo:
Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B
Resumo:
The intervalar arithmetic well-known as arithmetic of Moore, doesn't possess the same properties of the real numbers, and for this reason, it is confronted with a problem of operative nature, when we want to solve intervalar equations as extension of real equations by the usual equality and of the intervalar arithmetic, for this not to possess the inverse addictive, as well as, the property of the distributivity of the multiplication for the sum doesn t be valid for any triplet of intervals. The lack of those properties disables the use of equacional logic, so much for the resolution of an intervalar equation using the same, as for a representation of a real equation, and still, for the algebraic verification of properties of a computational system, whose data are real numbers represented by intervals. However, with the notion of order of information and of approach on intervals, introduced by Acióly[6] in 1991, the idea of an intervalar equation appears to represent a real equation satisfactorily, since the terms of the intervalar equation carry the information about the solution of the real equation. In 1999, Santiago proposed the notion of simple equality and, later on, local equality for intervals [8] and [33]. Based on that idea, this dissertation extends Santiago's local groups for local algebras, following the idea of Σ-algebras according to (Hennessy[31], 1988) and (Santiago[7], 1995). One of the contributions of this dissertation, is the theorem 5.1.3.2 that it guarantees that, when deducing a local Σ-equation E t t in the proposed system SDedLoc(E), the interpretations of t and t' will be locally the same in any local Σ-algebra that satisfies the group of fixed equations local E, whenever t and t have meaning in A. This assures to a kind of safety between the local equacional logic and the local algebras
Resumo:
The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification
Resumo:
Considering a non-relativistic ideal gas, the standard foundations of kinetic theory are investigated in the context of non-gaussian statistical mechanics introduced by Kaniadakis. The new formalism is based on the generalization of the Boltzmann H-theorem and the deduction of Maxwells statistical distribution. The calculated power law distribution is parameterized through a parameter measuring the degree of non-gaussianity. In the limit = 0, the theory of gaussian Maxwell-Boltzmann distribution is recovered. Two physical applications of the non-gaussian effects have been considered. The first one, the -Doppler broadening of spectral lines from an excited gas is obtained from analytical expressions. The second one, a mathematical relationship between the entropic index and the stellar polytropic index is shown by using the thermodynamic formulation for self-gravitational systems
Resumo:
Considering a quantum gas, the foundations of standard thermostatistics are investigated in the context of non-Gaussian statistical mechanics introduced by Tsallis and Kaniadakis. The new formalism is based on the following generalizations: i) Maxwell- Boltzmann-Gibbs entropy and ii) deduction of H-theorem. Based on this investigation, we calculate a new entropy using a generalization of combinatorial analysis based on two different methods of counting. The basic ingredients used in the H-theorem were: a generalized quantum entropy and a generalization of collisional term of Boltzmann equation. The power law distributions are parameterized by parameters q;, measuring the degree of non-Gaussianity of quantum gas. In the limit q
Resumo:
Among several theorems which are taught in basic education some of them can be proved in the classroom and others do not, because the degree of difficulty of its formal proof. A classic example is the Fundamental Theorem of Algebra which is not proved, it is necessary higher-level knowledge in mathematics. In this paper, we justify the validity of this theorem intuitively using the software Geogebra. And, based on [2] we will present a clear formal proof of this theorem that is addressed to school teachers and undergraduate students in mathematics
Resumo:
In this paper we analyze the Euler Relation generally using as a means to visualize the fundamental idea presented manipulation of concrete materials, so that there is greater ease of understanding of the content, expanding learning for secondary students and even fundamental. The study is an introduction to the topic and leads the reader to understand that the notorious Euler Relation if inadequately presented, is not sufficient to establish the existence of a polyhedron. For analyzing some examples, the text inserts the idea of doubt, showing cases where it is not fit enough numbers to validate the Euler Relation. The research also highlights a theorem certainly unfamiliar to many students and teachers to research the polyhedra, presenting some very simple inequalities relating the amounts of edges, vertices and faces of any convex polyhedron, which clearly specifies the conditions and sufficient necessary for us to see, without the need of viewing the existence of the solid screen. And so we can see various polyhedra and facilitate understanding of what we are exposed, we will use Geogebra, dynamic application that combines mathematical concepts of algebra and geometry and can be found through the link http://www.geogebra.org
Resumo:
We discuss an old theorem of Obrechkoff and some of its applications. Some curious historical facts around this theorem are presented. We make an attempt to look at some known results on connection coefficients, zeros and Wronskians of orthogonal polynomials from the perspective of Obrechkoff's theorem. Necessary conditions for the positivity of the connection coefficients of two families of orthogonal polynomials are provided. Inequalities between the kth zero of an orthogonal polynomial p(n)(x) and the largest (smallest) zero of another orthogonal polynomial q(n)(x) are given in terms of the signs of the connection coefficients of the families {p(n)(x)} and {q(n)(x)}, An inequality between the largest zeros of the Jacobi polynomials P-n((a,b)) (x) and P-n((alpha,beta)) (x) is also established. (C) 2001 Elsevier B.V. B.V. All rights reserved.
Resumo:
Let 0
Resumo:
Denote by x(n,k)(alpha, beta) and x(n,k) (lambda) = x(n,k) (lambda - 1/2, lambda - 1/2) the zeros, in decreasing order, of the Jacobi polynomial P-n((alpha, beta))(x) and of the ultraspherical (Gegenbauer) polynomial C-n(lambda)(x), respectively. The monotonicity of x(n,k)(alpha, beta) as functions of a and beta, alpha, beta > - 1, is investigated. Necessary conditions such that the zeros of P-n((a, b)) (x) are smaller (greater) than the zeros of P-n((alpha, beta))(x) are provided. A. Markov proved that x(n,k) (a, b) < x(n,k)(α, β) (x(n,k)(a, b) > x(n,k)(alpha, beta)) for every n is an element of N and each k, 1 less than or equal to k less than or equal to n if a > alpha and b < β (a < alpha and b > beta). We prove the converse statement of Markov's theorem. The question of how large the function could be such that the products f(n)(lambda) x(n,k)(lambda), k = 1,..., [n/2] are increasing functions of lambda, for lambda > - 1/2, is also discussed. Elbert and Siafarikas proved that f(n)(lambda) = (lambda + (2n(2) + 1)/ (4n + 2))(1/2) obeys this property. We establish the sharpness of their result. (C) 2002 Elsevier B.V. (USA).
Resumo:
Este trabalho é motivado pelo resultado de Berge, que é uma generalização do teorema de Tutte o qual expressamos na forma: Dado o grafo G de ordem |V(G)| eni(G) o número de arestas em um emparelhamento máximo, existe um conjunto X de vértices de G tal que |V(G)|+|X| - ômega(G\X) - 2n(G)=0, onde ômega(G\X) é o número de componentes de ordem ímpar de G\X. Tal expressão chamamos a equação de Tutte-Berge associada de G, e escrevemos simplesmente T(G; X)=0. Os grafos podem ser classificados a partir das soluções da equação de Tutte-Berge. Um grafo G é chamado imersível se, e somente se, T(G; X)=0 possui pelo menos um conjunto solução não vazio de vértices, e G é denominado não imersível se, e somente se, o conjunto vazio é a única solução de T(G; X)=0. O resultado principal deste artigo é a caracterização de grafos imersíveis pelos conjuntos antifatores completos, além disso, provamos que os grafos fatoráveis estão contidos na classe dos imersíveis.
Resumo:
Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)