共查询到20条相似文献,搜索用时 10 毫秒
1.
The first-order logical theory of dense linear order has long been known to admit quantifier elimination. This paper develops an explicit algorithm that yields an equivalent quantifier free form of its input formula. This algorithm performs existential quantifier elimination via constraint propagation. The result is computed incrementally using functional programming techniques. This approach may be of interest in implementing query languages for constraint databases. 相似文献
2.
In this paper, we present an out of order quantifier elimination algorithm for a class of Quantified Linear Programs (QLPs) called Standard Quantified Linear Programs (SQLPs). QLPs in general and SQLPs in particular are extremely useful constraint logic programming structures that find wide applicability in the modeling of real-time schedulability specifications; see Subramani [Subramani, K., 2005a. A comprehensive framework for specifying clairvoyance, constraints and periodicity in real-time scheduling. The Computer Journal 48 (3), 259–272]. Consequently any algorithmic advance in their solution has a strong practical impact. Prior to this work, the only known approaches to the solution of QLPs involved sequential variable elimination; see Subramani [Subramani, K., 2003b. An analysis of quantified linear programs. In: Calude, C.S. et al. (Eds.), Proceedings of the 4th International Conference on Discrete Mathematics and Theoretical Computer Science. DMTCS. In: Lecture Notes in Computer Science, vol. 2731. Springer-Verlag, pp. 265–277]. In the sequential approach, the innermost quantified variable is eliminated first, followed by the variable which then becomes the innermost quantified variable and so on, until we are left with a single variable from which the satisfiability of the original formula is easily deduced. This approach is applicable in both discrete and continuous domains; however, it is to be noted that the logic demanding the sequential approach requires that the variables are discrete-valued. To the best of our knowledge, the necessity for sequential elimination over continuous-valued variables has not been investigated in the literature. The techniques used in the development of our elimination algorithm may find applications in domains such as classical logic and finite model theory. The final aspect of our research concerns the structure-preserving nature of the algorithm that we introduce here; in general, it is not known whether discrete domains admit such elimination procedures. 相似文献
3.
An improved algorithm, together with its implementation, is presented for the automatic computation of the complete root classification of a real parametric polynomial. The algorithm offers improved efficiency and a new test for non-realizable conditions. The improvement lies in the direct use of ‘sign lists’, obtained from the discriminant sequence, rather than ‘revised sign lists’. It is shown that the discriminant sequences, upon which the sign lists are based, are closely related both to Sturm–Habicht sequences and to subresultant sequences. Thus calculations based on any of these quantities are essentially equivalent. 相似文献
4.
Adam Strzeboński 《Journal of Symbolic Computation》2011,46(11):1284-1290
We present a generalization of the Cylindrical Algebraic Decomposition (CAD) algorithm to systems of equations and inequalities in functions of the form p(x,f1(x),…,fm(x),y1,…,yn), where p∈Q[x,t1,…,tm,y1,…,yn] and f1(x),…,fm(x) are real univariate functions such that there exists a real root isolation algorithm for functions from the algebra Q[x,f1(x),…,fm(x)]. In particular, the algorithm applies when f1(x),…,fm(x) are real exp-log functions or tame elementary functions. 相似文献
5.
Tiwari (2004) proved that the termination problem of a class of linear programs (loops with linear loop conditions and updates) over the reals is decidable through Jordan forms and eigenvector computation. Braverman (2006) proved that it is also decidable over the integers. Following their work, we consider the termination problems of three more general classes of programs which are loops with linear updates and three kinds of polynomial loop conditions, i.e., strict constraints, non-strict constraints and both strict and non-strict constraints, respectively. First, we prove that the termination problems of such loops over the integers are all undecidable. Then, for each class we provide an algorithm to decide the termination of such programs over the reals. The algorithms are complete for those programs satisfying a property, Non-Zero Minimum. 相似文献
6.
7.
机器人技术中的碰撞问题可以被表示成量词消去问题,但由于有些碰撞问题的复杂性使得这些问题在单个微机上求解需要花费的时间很长或者根本就解不出来。本文提出了基于分布Maple系统下量词消去算法的并行化.并针对分布Maple系统的特点以及算法的特点,通过实例分析,给出了两种并行策略,以达到在Maple软件环境下提高处理器利用率,提高量词消去算法的效率的目的。 相似文献
8.
《国际计算机数学杂志》2012,89(4):433-461
VLSI technology has had tremendous success in revolutionizing computer design with processor arrays. Local communication and interconnection is a constraint that dictates the design of processor arrays. The shared bus and global access to memory are now no longer used, since they lower the speed. Consequently, parallel algorithms must be designed according to these constraints. One of the problems that must be resolved for the above mentioned constraints is data broadcast elimination. Algorithms must be transformed into a form that uses data propagation instead of data broadcast. Here systems of affine recurrence equations are analyzed and data broadcast is denned in context of the definition of data dependence and affine recurrence equations. A method for data broadcast elimination is introduced in [1] and expands the system of affine recurrence equations into new recurrence equations, that define data propagation and eliminates the data dependences where data broadcast occurs. Parallel algorithms are usually given as a set of similar tasks repetitively performed on different data. The iteration form of presenting the algorithms is most common. Several techniques are introduced to transform the algorithm to a single assignment form of recurrence equations. Some improvements of these techniques are presented to make the application of the data broadcast elimination method easier and more straight forward. The presented techniques are classified as the transformation of iterative algorithms to a recurrence form, the transformation of recurrence form to a single assignment form, and fulfilling the index forms of the algorithms. A system of affine recurrence equations with the data broadcast property is always obtained by applying these procedures. The method of data broadcast elimination successfully transforms this system of affine recurrence equations into a system of uniform recurrence equations which can be used for parallel implementation on VLSI processor arrays. 相似文献
9.
Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction 总被引:2,自引:0,他引:2
Mark E. Stickel 《Journal of Automated Reasoning》1994,13(2):189-210
Typical bottom-up, forward-chaining reasoning systems such as hyperresolution lack goaldirectedness, while typical top-down, backward-chaining reasoning systems like Prolog or model elimination repeatedly solve the same goals. Reasoning systems that are goal-directed and avoid repeatedly solving the same goals can be constructed by formulating the top-down methods meta-theoretically for execution by a bottom-up reasoning system (hence, we use the term upside-down meta-interpretation). This formulation also facilitates the use of flexible search strategies, such as merit-ordered search, that are common to bottom-up reasoning systems. The model elimination theorem-proving procedure, its extension by an assumption rule for abduction, and its restriction to Horn clauses are adapted here for such upside-down meta-interpretation. This work can be regarded as an extension of the magic-sets or Alexander method for query evaluation in deductive databases to both non-Horn clauses and abductive reasoning.This research was supported by the National Science Foundation under Grant CCT-8922330 and by the Defense Advanced Research Projects Agency under Office of Naval Research Contract N00014-90-C-0220. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the National Science Foundation, the Defense Advanced Research Projects Agency, or the United States Government. 相似文献
10.
11.
In this paper, we propose Unbiased Weighted Mean Filter (UWMF) for removing high-density impulse noise. Asymmetric distribution of corrupted pixels in the filtering window creates a spatial-bias towards the center of uncorrupted pixels. UWMF eliminates this bias by recalibrating the contribution factor (weight) of each uncorrupted pixel in such a way that the center shifts back to the center of the filtering window. The restoration process involves three sequential operations while convolving a filtering window over a contaminated image. Noise is detected, weights are recalibrated and the new intensity value is replaced by weighted mean using the recalibrated weights. Compared to the state-of-the-art impulse noise removal methods, UWMF provides superior performance, without requiring a fine-tuning for its parameters, in terms of both objective measurements and subjective assessments. 相似文献
12.
《国际计算机数学杂志》2012,89(1):29-44
In this paper a systolic array is presented for the solution of linear equations occurring in scientific and engineering calculations. The new systolic array is based on the parallel Quadrant Interlocking Elimination method of Evans and Hadjidimos [1]. 相似文献
13.
The β-fluoroamines are commonly used as substrate analogs to determine the mechanistic details of enzymatic reactions. Presence of fluorine atom gives rise to the alterations in the electronic profile and the pKa of molecules which results in mechanistic deviations. The fluorine-substituted mechanism-based substrate analogs are widely used in the inactivation of pyridoxal 5′-phosphate (PLP)-dependent enzymes. The presence of fluorine atom also alters the sequence of reactions taking place in PLP-dependent enzymes where the HF elimination reaction appears in between the transimination and inactivation reactions. Despite the amount of the works on β-fluoroamines, the effect of stereoelectronic differences on the transimination and HF elimination reactions taking place in PLP-dependent enzymes has not been investigated yet. A density functional theory study is conducted to elucidate mechanistic details of the reactions occurring in PLP-dependent enzymes. In order to understand the mechanistic insights of different isomers and the effect of the fluorine atom, 4-amino-3-fluorobutanoic acid (3-F-GABA) enantiomers are chosen to be investigated besides 4-aminobutanoic acid (GABA), which is the natural substrate for γ-aminobutyric acid aminotransferase (GABA-AT). The investigated β-fluoroamines are the experimentally proposed potential inhibitors of PLP-dependent enzyme GABA-AT. 相似文献
14.
The method of elimination of unknowns in a system of linear inequalities is considered. This method is used to solve systems
of linear inequalities whose structure is defined by some graph. The concepts of terminal and intermediate graphs are introduced.
A new system of inequalities derived by eliminating a group of unknowns that correspond to these subgraphs is described.
Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 66–74, September–October, 1999. 相似文献
15.
Rami Melhem 《Parallel Computing》1987,4(3):339-343
Any factorization/back substitution scheme for the solution of linear systems consists of two phases which are different in nature, and hence may be inefficient for parallel implementation on a single computational network. The Gauss-Jordan elimination scheme unifies the nature of the two phases of the solution process and thus seems to be more suitable for parallel architectures, especially if reconfiguration of the communication pattern is not permitted. In this communication, a computational network for the Gauss-Jordan algorithm is presented. This network compares favorably with optimal implementations of the Gauss elimination/back substitution algorithm. 相似文献
16.
Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently. 相似文献
17.
18.
The identifiability of the delay parameter for nonlinear systems with a single constant time delay is analyzed. We show the existence of input–output equations and relate the identifiability of the delay parameter to their form. Explicit criteria based on rank calculations are formulated. The identifiability of the delay parameter is shown not to be directly related to the well-characterized identifiability/observability of the other system parameters/states. 相似文献
19.
Rup Narayan Ray Debashis Chatterjee Swapan Kumar Goswami 《Applied Soft Computing》2009,9(4):1315-1320
Harmonic elimination problem in PWM inverter is treated as an optimization problem and solved using particle swarm optimization (PSO) technique. The derived equation for computation of total harmonic distortion (THD) of the output voltage of PWM inverter is used as the objective function in the PSO algorithm. The objective function is minimized to contribute the minimum THD in the voltage waveform and the corresponding switching angles are computed. The method is applied to investigate the switching patterns of both unipolar and bipolar case. While minimizing the objective function, the individual selected harmonics like 5th, 7th, 11th and 13th can be controlled within the allowable limits by incorporating the constraints in the PSO algorithm. The results of the unipolar case using five switching angles are compared with that of a recently reported work and it is observed that the proposed method is effective in reducing the voltage THD in a wide range of modulation index. The simulated results are also validated through suitable experiments. 相似文献
20.
任建强 《计算机工程与应用》2010,46(36):188-191
精确地消除活动阴影对运动目标的影响是智能视频监控的核心任务之一,对此提出了一种基于局部纹理分析的自适应阴影消除新算法。进行了基于高斯混合模型的背景重建,并根据阴影的光学特性进行了阴影区域的预检测,得到疑似阴影区域;提出了一种新的自适应动态纹理分析方法并在此基础上实现了活动阴影的检测与消除。实验结果验证了算法的有效性和实用性。 相似文献