Explore the vast range of titles available.

In this paper natural necessary and sufficient conditions for quantifier elimination of matrix rings M n ( K ) in the language of rings expanded by two unary functions, naming the trace and transposition, are identified. This is used together with invariant theory to prove quantifier elimination when K is an intersection of real closed fields. On the other hand, it is shown that finding a natural definable expansion with quantifier elimination of the theory of M n ( C ) is closely related to the infamous simultaneous conjugacy problem in matrix theory. Finally, for various natural structures describing dimension-free matrices it is shown that no such elimination results can hold by establishing undecidability results.

We present a framework for tame geometry on Henselian valued fields, which we call Hensel minimality. In the spirit of o-minimality, which is key to real geometry and several diophantine applications, we develop geometric results and applications for Hensel minimal structures that were previously known only under stronger, less axiomatic assumptions. We show the existence of t-stratifications in Hensel minimal structures and Taylor approximation results that are key to non-Archimedean versions of Pila–Wilkie point counting, Yomdin’s parameterization results and motivic integration. In this first paper, we work in equi-characteristic zero; in the sequel paper, we develop the mixed characteristic case and a diophantine application.

This paper is dedicated to studying the algorithmic properties of unars with an injective function. We prove that the theory of every such unar admits quantifier elimination if the language is extended by a countable set of predicate symbols. Necessary and sufficient conditions are established for the quantifier elimination to be effective, and a criterion for decidability of theories of such unars is formulated. Using this criterion, we build a unar such that its theory is decidable, but the theory of the unar of its subsets is undecidable.

In the current paper we consider theories with vocabulary containing a number of binary and unary relation symbols. Binary relation symbols represent labeled edges of a graph and unary relations represent unique annotations of the graph's nodes. Such theories, which we call annotation theories^ can be used in many applications, including the formalization of argumentation, approximate reasoning, semantics of logic programs, graph coloring, etc. We address a number of problems related to annotation theories over finite models, including satisfiability, querying problem, specification of preferred models and model checking problem. We show that most of considered problems are NPTime- or co-NPTime-complete. In order to reduce the complexity for particular theories, we use second-order quantifier elimination. To our best knowledge none of existing methods works in the case of annotation theories. We then provide a new second-order quantifier elimination method for stratified theories, which is successful in the considered cases. The new result subsumes many other results, including those of [2, 28, 21].

Probabilistic logic programming is a major part of statistical relational artificial intelligence, where approaches from logic and probability are brought together to reason about and learn from relational domains in a setting of uncertainty. However, the behaviour of statistical relational representations across variable domain sizes is complex, and scaling inference and learning to large domains remains a significant challenge. In recent years, connections have emerged between domain size dependence, lifted inference and learning from sampled subpopulations. The asymptotic behaviour of statistical relational representations has come under scrutiny, and projectivity was investigated as the strongest form of domain size dependence, in which query marginals are completely independent of the domain size. In this contribution we show that every probabilistic logic program under the distribution semantics is asymptotically equivalent to an acyclic probabilistic logic program consisting only of determinate clauses over probabilistic facts. We conclude that every probabilistic logic program inducing a projective family of distributions is in fact everywhere equivalent to a program from this fragment, and we investigate the consequences for the projective families of distributions expressible by probabilistic logic programs.

Background:: An application of a novel method of a quantifier elimination in epidemiology was presented in this paper Objective: We investigated the existence of the endemic equilibrium for the SEIRS model by QE method and gave a short review of the epidemic prediction models for covid-19. Methods: A new method for quantifier elimination for the theory of real closed fields. Results: Obtained value of a reproduction number and endemic equilibrium for the SEIRS model by QEAnalysis of the SEIR model with the concrete values through the example of Severe Acute Respiratory Syndrome (SARS) (a critical value of a transmission rate is evaluated in the example). Conclusion: The main result of this paper is the obtained value of the endemic equilibrium for the SEIRS model (similar result is obtained for the SEIR model). Also, we have analysed the SEIR model through the examle of SARS and we reviewed several epidemic prediction models for covid-19.

Bounds for positive definite sets such as attractors of dynamic systems are typically characterized by Lyapunov-like functions. These Lyapunov functions and their time derivatives must satisfy certain definiteness conditions, whose verification usually requires considerable experience. If the system and a Lyapunov-like candidate function are polynomial, the definiteness conditions lead to Boolean combinations of polynomial equations and inequalities with quantifiers that can be formally solved using quantifier elimination. Unfortunately, the known algorithms for quantifier elimination require considerable computing power, meaning that many problems cannot be solved within a reasonable amount of time. In this context, it is particularly important to find a suitable mathematical formulation of the problem. This article develops a method that reduces the expected computational effort required for the necessary verification of definiteness conditions. The approach is illustrated using the example of the Chua system with cubic nonlinearity.

Background: An application of a novel method of a quantifier elimination for the SEIS model was presented in this paper. The appearance of the AIDS disease was crucial for developing numerous new epidemic models. We decided to analyse one of these complex models by QE method. Objective: A main aim was to investigate the existence of the Hopf bifurcation for the SEIS model. We have also analysed one complex epidemic model appropriate for AIDS disease by QE method. We applied the SEIR model in order to analyse the early phase of COVID-19 in BiH and different regions in Italy. Methods: The implementation of a new method for quantifier elimination for the theory of real closed fields (a method was implemented in Mathematica). Results: The main result was that the system which describes the SEIS model does not have a Hopf bifurcation for any parameter values for the epidemiological relevant cases. Conclusion: We applied an original implementation of QE method successfully in order to investigate the SEIS model. Considering the application of QE method to a model appropriate for AIDS disease, we were interested in change of the qualitative behaviour of a parametrized system of differential equations.

We show that positivity (≥0) on R+n and on Rn of real symmetric polynomials of degree at most p in n≥2 variables is solvable by algorithms running in polynomial time in the number n of variables. For real symmetric quartics, we find discriminants which lead to the efficient algorithms QE4+ and QE4 running in O(n) time. We describe the Maple implementation of both algorithms, which are then used not only for testing concrete inequalities (with given numerical coefficients and number of variables), but also for proving symbolic inequalities.