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:
(纸本)9781538626269
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.
symbolic Computation (Mathematics Subject Classification 2000, 68W30) is often treated as just another subject in the wide field of special topics within mathematics;on the same level as mesh generation (65L50) or qua...
详细信息
ISBN:
(纸本)9780769546308
symbolic Computation (Mathematics Subject Classification 2000, 68W30) is often treated as just another subject in the wide field of special topics within mathematics;on the same level as mesh generation (65L50) or quasi-Frobenius rings (16L60). Here we want to argue that actually symbolic Compuation is not so much a topic in mathematics, but a relatively novel approach to mathematical epistemology;a different and, as we believe, fruitful way of looking at mathematics and the acquisition of knowledge in mathematics.
Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of logical formulas. Driven by the impressive success of SAT solvers for propositional logic, Satisfiability-Modulo-theories...
详细信息
ISBN:
(纸本)9781538626269
Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of logical formulas. Driven by the impressive success of SAT solvers for propositional logic, Satisfiability-Modulo-theories (SMT) solvers were developed to extend the scope also to different theories. Today, SMT solving is widely used in many applications, for example verification, synthesis, planning or product design automation. In this tutorial paper we give a short introduction to the foundations of SMT solving, describe some popular SMT solvers and illustrate their usage. We also present our own solver SMT-RAT, which was developed to support the strategic combination of different decision procedures, putting a focus on arithmetic theories.
this paper makes a short overview of current state of the art monitoring tools for cloud and big data frameworks. In order to effectively create, test and deploy new algorithms or frameworks one needs suitable monitor...
详细信息
ISBN:
(纸本)9781509004614
this paper makes a short overview of current state of the art monitoring tools for cloud and big data frameworks. In order to effectively create, test and deploy new algorithms or frameworks one needs suitable monitoring solutions. Hence we aim on creating a critical overview for some of the monitoring solutions existing on the market. Also we present relevant metrics used for monitoring cloud and big data applications, focused mainly on cloud deployment scenarios for big data frameworks.
We propose a new technique for identifying frequent patterns that occur in large transactional data sets using Boolean algebras. Our approach, which involves extending the notion of support from sets of attributes to ...
详细信息
ISBN:
(纸本)9781538626269
We propose a new technique for identifying frequent patterns that occur in large transactional data sets using Boolean algebras. Our approach, which involves extending the notion of support from sets of attributes to Boolean functions is more expressive than the standard approach that amounts to a search for conjunctive patterns. An efficient algorithm based on computing supports for minterms is presented. Also, we discuss an application of this algorithm to finding independent sets in graphs.
In the design of symbolic mathematical computation systems, it is a popular choice to use the same syntax for both mathematical indeterminates and programming variables. While mathematical indeterminates are to be use...
详细信息
ISBN:
(纸本)9781665465458
In the design of symbolic mathematical computation systems, it is a popular choice to use the same syntax for both mathematical indeterminates and programming variables. While mathematical indeterminates are to be used without specific values, programming variables must be initialized before being used in expressions. A problem occurs when mistakenly uninitialized programming variables are silently taken to be mathematical indeterminates. this article explores how this problem can arise and its consequences. An algorithm to analyze programs for this defect is shown along with a Maple implementation.
Service oriented architectures become more and more popular withthe emergence and consolidation of new paradigms such as Clouds and Grids. In this context scheduling becomes an important and difficult problem as serv...
详细信息
ISBN:
(纸本)9780769539645
Service oriented architectures become more and more popular withthe emergence and consolidation of new paradigms such as Clouds and Grids. In this context scheduling becomes an important and difficult problem as services hide their actual implementation, requirements or efficiency and are spread across multiple institutions and geographical locations. this paper proposes a distributed scheduling approach based on agents where each agent handles a certain domain and manages independently the policies inside it. In its frame several scheduling algorithms are also studied, compared and some results are given.
As an extension of our previous work on imperative program verification, we present a formalism for handling the total correctness of While loops in imperative programs, consisting in functional based definitions of t...
详细信息
ISBN:
(纸本)9780769539645
As an extension of our previous work on imperative program verification, we present a formalism for handling the total correctness of While loops in imperative programs, consisting in functional based definitions of the verification conditions for both partial correctness and for termination. A specific feature of our approach is the generation of verification conditions as first order formulae, including the termination condition which is expressed as an induction principle.
Satisfiability Checking is a relatively young research area, aiming at the development of efficient software technologies for checking the satisfiability of existentially quantified logical formulas. Besides the succe...
详细信息
ISBN:
(纸本)9781509057078
Satisfiability Checking is a relatively young research area, aiming at the development of efficient software technologies for checking the satisfiability of existentially quantified logical formulas. Besides the success story of SAT solving for propositional logic, SAT-modulo-theories (SMT) solvers offer sophisticated solutions for different theories. When targeting arithmetic theories, SMT solvers also make use of decision procedures rooted in symbolic Computation. In this paper we give a brief introduction to SMT solving, discuss differences to symbolic Computation, and illustrate the potentials and obstacles for embedding symbolic Computation techniques in SMT solving on the example of the Cylindrical Algebraic Decomposition.
While much is written about the importance of sparse polynomials in computer algebra, much less is known about the complexity of advanced (i.e. anything more than multiplication!) algorithms for them. this is due to a...
详细信息
ISBN:
(纸本)9780769539645
While much is written about the importance of sparse polynomials in computer algebra, much less is known about the complexity of advanced (i.e. anything more than multiplication!) algorithms for them. this is due to a variety of factors, not least the problems posed by cyclotomic polynomials. In this paper we state a few of the challenges that sparse polynomials pose.
暂无评论