In my PhD thesis 1965 and the subsequent publication 1970 in Aequationes Mathematicae, I introduced the notion of Grobner bases and proved a characterization theorem for Grobner bases on which an algorithm for constru...
详细信息
ISBN:
(纸本)9781538626269
In my PhD thesis 1965 and the subsequent publication 1970 in Aequationes Mathematicae, I introduced the notion of Grobner bases and proved a characterization theorem for Grobner bases on which an algorithm for constructing Grobner bases can be based. the main idea for the theorem and the algorithm was the notion of \"�S-polynomials\"�. Most of the subsequent work on the algorithmic theory of Grobner bases, including the implementation of the Grobner bases technology in mathematical software systems like Mathematica, Maple, etc. was based on this approach.
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.
Widespreading and enabling machine processing of old prints relevant to a particular cultural area can be achieved using modern research infrastructures. this paper outlines the architecture of a distributed environme...
详细信息
ISBN:
(纸本)9781538626269
Widespreading and enabling machine processing of old prints relevant to a particular cultural area can be achieved using modern research infrastructures. this paper outlines the architecture of a distributed environment for optical character recognition customized for a collection comprising scanned books in old Romanian language and it also presents the preliminary results of our experiments.
there is little doubt that, in the minds of most symbolic computation researchers, the ideal paper consists of a problem statement, a new algorithm, a complexity analysis and preferably a few validating examples. ther...
详细信息
ISBN:
(纸本)9781728106267
there is little doubt that, in the minds of most symbolic computation researchers, the ideal paper consists of a problem statement, a new algorithm, a complexity analysis and preferably a few validating examples. there are many such great papers. this paradigm has served computer algebra well for many years, and indeed continues to do so where it is applicable. However, it is much less applicable to sparse problems, where there are many NP-hardness results, or to many problems coming from algebraic geometry, where the worst-case complexity seems to be rare. We argue that, in these cases, the field should take a leaf out of the practices of the SAT-solving community, and adopt systematic benchmarking, and benchmarking contests, as a way measuring (and stimulating) progress. this would involve a change of culture.
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.
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.
We define a new bio-inspired computational model for deciding 2-dimensional languages that is directly derived from the one in [13]. the described model has a slightly different accepting protocol as the previous one ...
详细信息
ISBN:
(纸本)9781538626269
We define a new bio-inspired computational model for deciding 2-dimensional languages that is directly derived from the one in [13]. the described model has a slightly different accepting protocol as the previous one and, besides the deletion and substitution operations, we now consider a new type of operation, namely circular permutation. We show that by using circular permutations, such networks can recognize any input that contains a given sub-picture as where our previous model limited one of the pattern dimensions to a size of at most 3.
Proof schemata are a variant of LK-proofs able to simulate various induction schemes in first-order logic by adding so called links to the standard first-order LK-calculus. Links allow proofs to reference other proofs...
详细信息
ISBN:
(纸本)9781538626269
Proof schemata are a variant of LK-proofs able to simulate various induction schemes in first-order logic by adding so called links to the standard first-order LK-calculus. Links allow proofs to reference other proofs, and thus give schemata a recursive structure. Gentzen style cut-elimination methods, which reduce cuts locally, does not work in the presence of links. However, an alternative method, such as cut-elimination by resolution (CERES), which eliminate cuts globally, is able to reduce cuts over the entire recursive structure simultaneously. Unfortunately, analysis of the cut structure of a proof after partial cut-elimination is non-trivial. By extending local methods to proof schemata, we provide such an analysis.
Verifying arithmetic circuits is an important problem which still requires considerable manual effort. For instance multipliers are considered difficult to verify. the currently most effective approach for arithmetic ...
详细信息
ISBN:
(纸本)9781538626269
Verifying arithmetic circuits is an important problem which still requires considerable manual effort. For instance multipliers are considered difficult to verify. the currently most effective approach for arithmetic circuit verification uses computer algebra. In this approach the circuit is modeled as a set of pseudo-boolean polynomials and it is checked if the given word-level specification is implied by the circuit polynomials. For this purpose the theory of Grobner bases is used. In this paper we give a summary of two recent papers on this work. We reword the theory and illustrate the results of these papers by examples. We also present a new technical theorem which allows to rewrite local parts of the Grobner basis. Rewriting the Grobner basis has tremendous effect on computation time.
the advent of emerging information and communication technologies, such as RFID, small size sensors and sensor networks, has made accessible a huge amount of information that requires sophisticated and efficient searc...
详细信息
ISBN:
(纸本)9781538626269
the advent of emerging information and communication technologies, such as RFID, small size sensors and sensor networks, has made accessible a huge amount of information that requires sophisticated and efficient search algorithms to support queries on that data. In this paper we focus on the problem of aggregating data collected from these devices to efficiently support queries, inferences or statistics on them. In general, data aggregation techniques are necessary to efficiently collect information in a compact and cost-effective way. Some current solutions try to meet the above criteria, by exploiting different data aggregation techniques, for instance BitVector or Q_Digest. In this manuscript, we exploit the mathematical wavelet structure to define a sophisticated data aggregation technique for information collected from different nodes. the aggregated data is then exploited for solving multidimensional range queries. Experimental results based on simulations of a real dataset show the effectiveness of our approach with respect to other aggregation strategies.
暂无评论