ksmt is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this article we investigate properties of the ksmt calculus and show that it is a δ-complete decision procedure for bounded problems. For that purpose we provide concrete algorithms computing linearisations based on either uniform or local moduli of continuity of non-linear functions. The latter method is called local linearisation and is shown to have desirable properties sufficient for termination and which also allow for more efficient treatment of non-linear constraints. Our methods for constructing linearisations are based on computable analysis, in particular we introduce the Cauchy-compatible compact representation of reals and prove its names to be locally compact, allowing for more efficient computation of local linearisations while maintaining δ-completeness.

Abstract is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the calculus and show that it is a $$\delta $$ δ -complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.

In the framework of effectively enumerable topological spaces, we introduce the notion of a partial computable function. We show that the class of partial computable functions is closed under composition, and the real-valued partial computable functions defined on a computable Polish space have a principal computable numbering. With respect to the principal computable numbering of the real-valued partial computable functions, we investigate complexity of important problems such as totality and root verification. It turns out that for some problems the corresponding complexity does not depend on the choice of a computable Polish space, whereas for other ones the corresponding choice plays a crucial role.

We provide requirements on effectively enumerable topological spaces which guarantee that the Rice-Shapiro theorem holds for the computable elements of these spaces. We show that the relaxation of these requirements leads to the classes of effectively enumerable topological spaces where the Rice-Shapiro theorem does not hold. We propose two constructions that generate effectively enumerable topological spaces with particular properties from wn--families and computable trees without computable infinite paths. Using them we propose examples that give a flavor of this class.

This issue of Mathematical Structures in Computer Science is composed mainly of papers submitted by participants of the Workshop ‘Continuity, Computability, Constructivity: From Logic to Algorithms,’ held in Gregynog, a conference centre of the University of Wales located in the beautiful nature of Mid Wales, in the last week of June 2013. In addition, several colleagues accepted our invitation to contribute to this volume.

This paper is a part of the ongoing program of analysing the complexity of various problems in computable analysis in terms of the complexity of the associated index sets. In the framework of effectively enumerable topological spaces, we investigate the following question: given an effectively enumerable topological space whether there exists a computable numbering of all its computable elements. We present a natural sufficient condition on the family of basic neighbourhoods of computable elements that guarantees the existence of a principal computable numbering. We show that weakly-effective ω–continuous domains and the natural numbers with the discrete topology satisfy this condition. We prove weak and strong analogues of Rice's theorem for computable elements. Then, we construct principal computable numberings of partial majorant-computable real-valued functions and co-effectively closed sets and calculate the complexity of index sets for important problems such as root verification and function equality. For example, we show that, for partial majorant-computable real functions, the equality problem is Π 1 1 -complete.

In this paper, we develop a general framework for continuous data representations using positive predicate structures. We first show that basic principles of Σ-definability which are used to investigate computability, i.e., existence of a universal Σ-predicate and an algorithmic characterization of Σ-definability hold on all predicate structures without equality. Then we introduce positive predicate structures and show connections between these structures and effectively enumerable topological spaces. These links allow us to study computability over continuous data using logical and topological tools.

We consider the solution of initial value problems within the context of hybrid systems and emphasise the use of high precision approximations (in software for exact real arithmetic). We propose a novel algorithm for the computation of trajectories up to the area where discontinuous jumps appear, applicable for holomorphic flow functions. Examples with a prototypical implementation illustrate that the algorithm might provide results with higher precision than well-known ODE solvers at a similar computation time.

This article is an extended version of the paper published in Korovina and Kudinov (2007, Lecture Notes in Computer Science, Vol. 4497, pp. 416–425). The main goal of this research is to develop logical tools and techniques for effective reasoning about continuous data based on Σ-definability. In this article we invent the Uniformity Principleand prove it for Σ-definability over the real numbers extended by open predicates. Using the Uniformity Principle, we investigate different approaches to enrich the language of Σ-formulas in such a way that simplifies reasoning about computable continuous data without enlarging the class of Σ-definable sets. In order to do reasoning about computability of certain continuous data we have to pick up an appropriate language of a structure representing these continuous data. We formulate several major conditions how to do that in a right direction. We also employ the Uniformity Principleto argue that our logical approach is a good way for formalization of computable continuous data in logical terms.