8 resultados para proofs
em Biblioteca Digital da Produção Intelectual da Universidade de São Paulo (BDPI/USP)
Resumo:
The logic of proofs (lp) was proposed as Gdels missed link between Intuitionistic and S4-proofs, but so far the tableau-based methods proposed for lp have not explored this closeness with S4 and contain rules whose analycity is not immediately evident. We study possible formulations of analytic tableau proof methods for lp that preserve the subformula property. Two sound and complete tableau decision methods of increasing degree of analycity are proposed, KELP and preKELP. The latter is particularly inspired on S4-proofs. The crucial role of proof constants in the structure of lp-proofs methods is analysed. In particular, a method for the abduction of proof constant specifications in strongly analytic preKELP proofs is presented; abduction heuristics and the complexity of the method are discussed.
Resumo:
In this paper we give general results on the continuity of pullback attractors for nonlinear evolution processes. We then revisit results of [D. Li, P.E. Kloeden, Equi-attraction and the continuous dependence of pullback attractors on parameters, Stoch. Dyn. 4 (3) (2004) 373-384] which show that, under certain conditions, continuity is equivalent to uniformity of attraction over a range of parameters (""equi-attraction""): we are able to simplify their proofs and weaken the conditions required for this equivalence to hold. Generalizing a classical autonomous result [A.V. Babin, M.I. Vishik, Attractors of Evolution Equations, North Holland, Amsterdam, 1992] we give bounds on the rate of convergence of attractors when the family is uniformly exponentially attracting. To apply these results in a more concrete situation we show that a non-autonomous regular perturbation of a gradient-like system produces a family of pullback attractors that are uniformly exponentially attracting: these attractors are therefore continuous, and we can give an explicit bound on the distance between members of this family. (C) 2009 Elsevier Ltd. All rights reserved.
Resumo:
A method for linearly constrained optimization which modifies and generalizes recent box-constraint optimization algorithms is introduced. The new algorithm is based on a relaxed form of Spectral Projected Gradient iterations. Intercalated with these projected steps, internal iterations restricted to faces of the polytope are performed, which enhance the efficiency of the algorithm. Convergence proofs are given and numerical experiments are included and commented. Software supporting this paper is available through the Tango Project web page: http://www.ime.usp.br/similar to egbirgin/tango/.
Resumo:
In this article dedicated to Professor V. Lakshmikantham on the occasion of the celebration of his 84th birthday, we announce new results concerning the existence and various properties of an evolution system UA+B(t, s)(0 <= s <= t <= T) generated by the sum -(A(t)+B(t)) of two linear, time-dependent and generally unbounded operators defined on time-dependent domains in a complex and separable Banach space B. In particular, writing G(B) for the algebra of all linear bounded operators on B, we can express UA+B(t, s)(0 <= s <= t <= T) as the strong limit in L(B) of a product of the holomorphic contraction semigroups generated by -A(t) and -B(t), thereby getting a product formula of the Trotter-Kato type under very general conditions which allow the domain D(A(t)+B(t)) to evolve with time provided there exists a fixed set D subset of boolean AND D-t epsilon[0,D-T](A(t)+B(t)) everywhere dense in B. We then mention several possible applications of our product formula to various classes of non-autonomous parabolic initial-boundary value problems, as well as to evolution problems of Schrodinger type related to the theory of time-dependent singular perturbations of self-adjoint operators in quantum mechanics. We defer all the proofs and all the details of the applications to a separate publication. (C) 2008 Elsevier Ltd. All rights reserved.
Resumo:
A Nonlinear Programming algorithm that converges to second-order stationary points is introduced in this paper. The main tool is a second-order negative-curvature method for box-constrained minimization of a certain class of functions that do not possess continuous second derivatives. This method is used to define an Augmented Lagrangian algorithm of PHR (Powell-Hestenes-Rockafellar) type. Convergence proofs under weak constraint qualifications are given. Numerical examples showing that the new method converges to second-order stationary points in situations in which first-order methods fail are exhibited.
Resumo:
In this work we investigate the relation between the fundamental group of a complete Riemannian manifold M and the quotient between the Weyl group and reflection group of a polar action on M, as well as the relation between the fundamental group of M and the quotient between the lifted Weyl group and lifted reflection group. As applications we give alternative proofs of two results. The first one, due to the author and Toben, implies that a polar action does not admit exceptional orbits, if M is simply connected. The second result, due to Lytchak, implies that the orbits are closed and embedded if M is simply connected. All results are proved in the more general case of polar foliations.
Resumo:
We consider polynomial identities satisfied by nonhomogeneous subalgebras of Lie and special Jordan superalgebras: we ignore the grading and regard the superalgebra as an ordinary algebra. The Lie case has been studied by Volichenko and Baranov: they found identities in degrees 3, 4 and 5 which imply all the identities in degrees <= 6. We simplify their identities in degree 5, and show that there are no new identities in degree 7. The Jordan case has not previously been studied: we find identities in degrees 3, 4, 5 and 6 which imply all the identities in degrees <= 6, and demonstrate the existence of further new identities in degree 7. our proofs depend on computer algebra: we use the representation theory of the symmetric group, the Hermite normal form of an integer matrix, the LLL algorithm for lattice basis reduction, and the Chinese remainder theorem. (C) 2009 Elsevier Inc. All rights reserved.
Resumo:
In this paper, we show the existence of new families of spatial central configurations for the n + 3-body problem, n >= 3. We study spatial central configurations where n bodies are at the vertices of a regular n-gon T and the other three bodies are symmetrically located on the straight line that is perpendicular to the plane that contains T and passes through the center of T. The results have simple and analytic proofs. (c) 2010 Elsevier Ltd. All rights reserved.