排序方式: 共有37条查询结果,搜索用时 15 毫秒
1.
2.
We show that it is decidable for any given ground term rewrite systems R and S if there is a ground term rewrite system U such that ↔U*=↔R*∩↔S*. If the answer is yes, then we can effectively construct such a ground term rewrite system U. In other words, for any given finitely generated congruences ρ and τ over the term algebra, it is decidable if ρ∩τ is a finitely generated congruence. If the answer is yes, then we can effectively construct a ground term rewrite system U such that ↔U*=ρ∩τ. 相似文献
3.
一种基于DTD的XPath逻辑优化方法 总被引:12,自引:1,他引:12
Xpath成为XML数据查询的基本机制.Xpath中表达节点之间的祖孙关系的‘//'和任意匹配字符的‘*'等非确定操作符,增强了Xpath表达方式的灵活性,但同时引入了Xpath处理的复杂性.如何利用DTD减少Xpath中的不确定操作符,从而提高Xpath的执行效率成为一个基本的研究问题.传统方法主要侧重于特定受限Xpath的确定化重写.利用树自动机在一个框架中表达Xpath和DTD,提出了一种新的Xpath树自动机和DTD树自动机的乘积运算,并证明了乘积的结果就是基于DTD的Xpath优化形式,在多项式时间内基于代价获取了Xpath的优化结果.实验数据表明,基于提出的Xpath的逻辑优化方法,能够有效地提高Xpath执行器的执行效率. 相似文献
4.
本文详细讨论了重写模块的设计思想与实现技术,并讨论了利用执行引擎特点引入的一组基于等价谓调的简单语句直写规则.测试结果表明,增加重写模块的查询优化器能显著提高系统的查询效率. 相似文献
5.
M.?ChemillierEmail author 《Soft Computing - A Fusion of Foundations, Methodologies and Applications》2004,8(9):617-622
This paper shows how to generate jazz chord sequences incrementally using Steedmans grammar by taking advantage of some formal properties. We point out the specific role played by particular chord sequences called cadential sequences. By precompiling them, one could improve the implementation of Steedmans grammar in a real-time improvisation system, and make it more reactive to the inputs of the user.I thank Mark Steedman for his comments on this text. 相似文献
6.
Ahmed Bouajjani Jan Strej
ek Tayssir Touili 《Electronic Notes in Theoretical Computer Science》2007,175(3):47
We consider the verification problem of a class of infinite-state systems called wPAD. These systems can be used to model programs with (possibly recursive) procedure calls and dynamic creation of parallel processes. They correspond to PAD models extended with an acyclic finite-state control unit, where PAD models can be seen as combinations of prefix rewrite systems (pushdown systems) with context-free multiset rewrite systems (synchronization-free Petri nets). Recently, we have presented symbolic reachability techniques for the class of PAD based on the use of a class of unranked tree automata. In this paper, we generalize our previous work to the class wPAD which is strictly larger than PAD. This generalization brings a positive answer to an open question on decidability of the model checking problem for wPAD against EF logic. Moreover, we show how symbolic reachability analysis of wPAD can be used in (under) approximate analysis of Synchronized PAD, a (Turing) powerful model for multithreaded programs (with unrestricted synchronization between parallel processes). This leads to a pragmatic approach for detecting the presence of erroneous behaviors in these models based on the bounded reachability paradigm where the notion of bound considered here is the number of synchronization actions. 相似文献
7.
Pierre Lescanne 《Journal of Automated Reasoning》1990,6(1):39-49
This paper studies three orderings, useful in theorem proving, especially for proving termination of term rewriting systems: the recursive decomposition ordering with status, the recursive path ordering with status and the closure ordering. It proves the transitivity of the recursive path ordering, the strict inclusion of the recursive path ordering in the recursive decomposition ordering, the totality of the recursive path ordering — therefore of the recursive decomposition ordering — the strict inclusion of the recursive decomposition ordering in the closure ordering and the stability of the closure ordering by instantiation.Part of this work was done while the author was visiting the Institute for New Generation Computer Technology, Tokyo, Japan. 相似文献
8.
Sándor Vágvölgyi 《Information Processing Letters》2008,108(5):264-272
The union of a monadic and a right-ground term rewrite system is called a murg term rewrite system. We show that for murg TRSs the ground common ancestor problem is undecidable. We show that for a murg term rewrite system it is undecidable whether the set of descendants of a ground tree is a recognizable tree language. We show that it is undecidable whether a murg term rewrite system over Σ preserves Σ-recognizability. 相似文献
9.
When rewriting is used to generate convergent and complete rewrite systems in order to answer the validity problem for some
theories, all the rewriting theories rely on a same set of notions, properties, and methods. Rewriting techniques have been
used mainly to answer the validity problem of equational theories, that is, to compute congruences. Recently, however, they
have been extended in order to be applied to other algebraic structures such as preorders and orders. In this paper, we investigate
an abstract form of rewriting, by following the paradigm of logical-system independency. To achieve this purpose, we provide a few simple conditions (or axioms) under which rewriting (and then the set of classical
properties and methods) can be modeled, understood, studied, proven, and generalized. This enables us to extend rewriting
techniques to other algebraic structures than congruences and preorders such as congruences closed under monotonicity and
modus ponens. We introduce convergent rewrite systems that enable one to describe deduction procedures for their corresponding
theory, and we propose a Knuth-Bendix–style completion procedure in this abstract framework. 相似文献
10.
Adaptive automated planning systems that can, over time, improve the quality of plans they produce are a promising prospect. The first part of the article discusses the issues involved in designing quality improving learning for planning systems and reviews recent work on learning to improve plan quality. The second part describes our work on the Performance Improving Planning (PIP) System. The heart of PIP is an analytic technique that compares two planning episodes for solving a planning problem that led to two different quality solutions—a higher-quality solution and a lower quality solution—and identifies the critical differences that were responsible for the resulting differences in the quality of the completed plans. We compare the effectiveness of two different ways of storing and applying the knowledge learned from this analysis—as search-control rules and as rewrite rules. The results show that the search-control rules are more effective in improving plan quality. Further analysis of PIP-search-control—the version of PIP that stores the learned knowledge as search-control rules—shows that it is an effective technique for improving plan quality in a variety of situations. 相似文献