there has been surprisingly little written about the practical use of Strassen–Winograd (as opposed to interpolation-based, and therefore oriented towards matrices of dense polynomials) fast matrix methods in ...
详细信息
ISBN:
(纸本)9781538626276
there has been surprisingly little written about the practical use of Strassen–Winograd (as opposed to interpolation-based, and therefore oriented towards matrices of dense polynomials) fast matrix methods in computer algebra. We show that Strassen–Winograd multiplication can be practically effective. We also derive a fraction-free method of fast matrix inversion, and investigate its efficiency.
A multi region finite difference method is described and applied to the one dimension, semi linear, singularly perturbed boundary value problem (SPBVP). the process of developing high precision algorithms for this pro...
详细信息
A multi region finite difference method is described and applied to the one dimension, semi linear, singularly perturbed boundary value problem (SPBVP). the process of developing high precision algorithms for this problem is described and it is shown that when the multi region method is combined withthe use of these high order algorithms, numerical solutions can achieve accuracies in the range of 10-20. this represents a gain of between 9 to 14 orders of magnitude over current techniques.
Gradient-based local optimization has been shown to improve results of genetic programming (GP) for symbolic regression. Several state-of-the-art GP implementations use iterative nonlinear least squares (NLS) algorith...
详细信息
Gradient-based local optimization has been shown to improve results of genetic programming (GP) for symbolic regression. Several state-of-the-art GP implementations use iterative nonlinear least squares (NLS) algorithms such as the Levenberg-Marquardt algorithm for local optimization. the effectiveness of NLS algorithms depends on appropriate scaling and conditioning of the optimization problem. this has so far been ignored in symbolic regression and GP literature. In this study we use a singular value decomposition of NLS Jacobian matrices to determine the numeric rank and the condition number. We perform experiments with a GP implementation and six different benchmark datasets. Our results show that rank-deficient and ill-conditioned Jacobian matrices occur frequently and for all datasets. the issue is less extreme when restricting GP tree size and when using many non-linear functions in the function set.
We introduce Venn diagrams for multisets and showhow they simplify the analysis of multisets. Venn diagrams arevery useful in proofs involving multisets and multiset orders, especially considering the complications in...
详细信息
We introduce Venn diagrams for multisets and showhow they simplify the analysis of multisets. Venn diagrams arevery useful in proofs involving multisets and multiset orders, especially considering the complications introduced by the multiplicity of elements in multisets. We compare the Venn diagramsfor multisets withthe corresponding ones for sets. thus, wepresent two types of Venn diagrams for multisets, a simple onethat looks like a diagram for sets, but with areas that are notnecessarily disjoint, and a complex one (compared to sets), butwith certain delimited disjoint areas.
We define the functional inverse of the Gamma function. It is a multivalued function, and we define its branches. We present its basic properties, included series approximations, asymptotic results and numerical evalu...
详细信息
ISBN:
(纸本)9781538626276
We define the functional inverse of the Gamma function. It is a multivalued function, and we define its branches. We present its basic properties, included series approximations, asymptotic results and numerical evaluation.
the development of software systems for scientific exploration and discovery through computation has an important issue to address: the management of underlying computational steps. To support composition of Web and G...
详细信息
the development of software systems for scientific exploration and discovery through computation has an important issue to address: the management of underlying computational steps. To support composition of Web and Grid services, standard workflow languages and workflow execution engines were built but management capabilities are not yet entirely explored. In the context of Grid services, we propose a solution for controlling the execution of workflows without the assistance of a user interface oriented workflow engine. We also investigate the capabilities that our solution may offer for related features such as dynamic retrieval of partial results, steering and provenance.
Summary form only given. We give a simple introduction to satisfiability modulo theories intended for non-specialists. No previous background is assumed. the tutorial covers the following topics. 1) Propositional sati...
详细信息
Summary form only given. We give a simple introduction to satisfiability modulo theories intended for non-specialists. No previous background is assumed. the tutorial covers the following topics. 1) Propositional satisfiability. 2) DPLL as the main method for satisfiability checking. 3) Implementations of DPLL. 4) theories. 5) Decision procedures for theories. Congruence closure, the theory of arrays and linear arithmetic. 6) SMT: satisfiability modulo theories. How to convert a decision procedure for a set of literals to a DPLL modulo theory algorithm. 7) Satisfiability in a combination of theories. Instead of proving theorems, we will try to explain the main ideas using examples. the tutorial serves as a background for the second tutorial by Nikolaj Bjorner "SMT solvers for Testing, Program Analysis and Verification at Microsoft".
ROC! is a deterministic rewrite strategy language which includes the rewrite rules as basic operators, and the deterministic choice and the repetition as high-level strategy operators. In this paper we present a metho...
详细信息
ROC! is a deterministic rewrite strategy language which includes the rewrite rules as basic operators, and the deterministic choice and the repetition as high-level strategy operators. In this paper we present a method which, for a given term Rewriting system (TRS) R, constructs a new TRS Rmacr such that R-rewriting is equivalent (sound and complete) with Rmacr-rewriting constrained by ROC!. Since Rmacr uses a stack, it is called a rewrite stack machine.
Data compression is used to reduce the cost of storing and transmitting increasingly large datasets in various domains ranging from bioinformatics to particle physics and general purpose computing. Most of these areas...
详细信息
Data compression is used to reduce the cost of storing and transmitting increasingly large datasets in various domains ranging from bioinformatics to particle physics and general purpose computing. Most of these areas require the ability to scan the datasets for patterns like DNA sequences, malicious executable code or various other string queries, an operation that is hindered by the altered form of the data. In order to speed up the matching process, several compressed pattern matching algorithms have been previously proposed. this paper presents an overview of the state of the art in multiple pattern matching of Lempel-Ziv-Welch encoded archives, together with experimental results.
Learning and backjumping are essential features in search-based decision procedures for Quantified Boolean Formulas (QBF). To obtain a better understanding of such procedures, we present a formal framework, which allo...
详细信息
ISBN:
(纸本)9781509057085
Learning and backjumping are essential features in search-based decision procedures for Quantified Boolean Formulas (QBF). To obtain a better understanding of such procedures, we present a formal framework, which allows to simultaneously reason on prenex conjunctive and disjunctive normal form. It captures both satisfying and falsifying search states in a symmetric way. this symmetry simplifies the framework and offers potential for further variants.
暂无评论