We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...
We present an efficient, modular, and feature-rich framework for automated generation and validation of complex structures, suitable for tasks that explore a large space of structured values. Our framework is capable of exhaustive, incremental, parallel, a ...
We present a performance analysis for image registration with gradient descent. We consider a typical multiscale registration setting where the global 2-D translation between a pair of images is estimated by smoothing the images and minimizing the distance ...
Schema and ontology matching is a process of establishing correspondences between schema attributes and ontology concepts, for the purpose of data integration. Various commercial and academic tools have been developed to support this task. These tools prov ...
We investigate systems of ordinary differential equations with a parameter. We show that under suitable assumptions on the systems the solutions are computable in the sense of recursive analysis. As an application we give a complete characterization of the ...
The authors define a family of functions by starting with (complex) exponentials and closing under some basic algebraic operations, integration, and solution of certain systems of differential equations. They then show that for every recursively (computabl ...
