XML压缩文档上的数值更新方法

近年来,XML已成为Web上信息交流和资源共享的主要载体。但XML自身的自冗余特性限制了它的普遍应用。目前,已经有研究成果提出了XML的压缩方法。压缩的XML文档能够有效利用存储空间,节省网络带宽。在实际应用中,经常需要对压缩存储的XML文档进行更新。对于大的压缩文档,如果先解压再更新,会消耗大量时间,因此,高效的更新方法应该避免解压缩文档,在压缩的XML文档上直接进行更新操作。本文针对压缩XML文档中的数值类型（包括整型和浮点型）数据,研究了在保持压缩状态条件下如何进行有效的数值更新,提出了基于XPRESS实现的Naive数值更新方法,以及修改XPRESS编码方法实现的更为高效的Pivot数值更新方法。通过大量的实验证明,Pivot数值更新方法不仅能够提供高效的更新处理,而且保持了XPRESS的高压缩率。     

一种数据流上截止期敏感的滑动窗口处理策略

在数据流上定义了截止期作为连续查询的实时约束,并建立了基于截止期的滑动窗口处理模型;提出了一种基于预测的截止期敏感的滑动窗口处理策略;在多滑动窗口查询处理环境中,提出了一种（k,m ）截止期约束机制,在提高查询实时性的前提下,尽可能的满足不同查询对结果丢失率的不同约束。实验结果表明该处理策略能够有效提高数据流上滑动窗口查询的截止期满足率。     

一种基于路径分块索引的XML查询方法

针对XML的相对路径查询及引用路径查询问题,提出了一种面向XML数据的路径分块索引KI。探讨了KI索引构造方法、索引节点分裂算法和相关查询处理的算法,并用VC++实现,利用Shakespeare和Xorder数据集进行了XML查询测试,实验结果表明,提出的KI索引能有效地提高XML查询效率。     

FFT处理机的形式化模型及正确性验证

快速傅立叶变换的应用领域非常广泛,其硬件实现方法多种多样,验证这些电路的正确性具有很强的实用价值。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是随着参与运算的点数的增加,穷尽模拟全部输入情况所耗费的时间越来越长,甚至难以实现。而形式化方法使用纯数学手段证明电路的正确性,克服了传统方法的缺点。首先用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,然后给出它的正确性验证,探索了验证处理复数的复杂电路正确性的方法。     

结合关系建模与项重写技术的时序电路等价验证

提出一个新颖的时序电路等价验证的方法框架.该方法有效地结合了关系建模和项重写技术.首先利用带有测试条件的Kleene关系代数建模时序设计,进而通过对关系表达式的项重写来证明时序设计的等价性.与传统的基于状态空间遍历的时序等价验证方法相比,该方法提供了一种全新的思路.     

Undecidable properties of flat term rewrite systems

Reachability, joinability and confluence properties are known to be undecidable for flat term rewrite systems (TRS). We give shorter and conceptually simpler proofs of these results. We also prove undecidability of weak normalization and unique normalization properties for flat TRS. The first author was supported by Spanish Ministry of Education and Science by the FORMALISM project (TIN2007-66523) and by the LOGICTOOLS-2 project (TIN2007-68093-C02-01). The second author was supported by Spanish Ministry of Education and Science by the FORMALISM project (TIN2007-66523).     

External Rewriting for Skeptical Proof Assistants

This paper presents the design, the implementation, and experiments of the integration of syntactic, conditional possibly associative-commutative term rewriting into proof assistants based on constructive type theory. Our approach is called external because it consists in performing term rewriting in a specific and efficient environment and checking the computations later in a proof assistant. Two typical systems are considered in this work: ELAN, based on the rewriting calculus, as the term rewriting-based environment, and Coq, based on the calculus of inductive constructions as the proof assistant. We first formalize the proof terms for deduction by rewriting and strategies in ELAN using the rewriting calculus with explicit substitutions. We then show how these proof terms can soundly be translated into Coq syntax where they can be directly type checked. For the method to be applicable for rewriting modulo associativity and commutativity, we provide an effective method to prove equalities modulo these axioms in Coq using ELAN. These results have been integrated into an ELAN-based rewriting tactic in Coq.     

Answering constraint-based mining queries on itemsets using previous materialized results

In recent years, researchers have begun to study inductive databases, a new generation of databases for leveraging decision support applications. In this context, the user interacts with the DBMS using advanced, constraint-based languages for data mining where constraints have been specifically introduced to increase the relevance of the results and, at the same time, to reduce its volume. In this paper we study the problem of mining frequent itemsets using an inductive database. We propose a technique for query answering which consists in rewriting the query in terms of union and intersection of the result sets of other queries, previously executed and materialized. Unfortunately, the exploitation of past queries is not always applicable. We then present sufficient conditions for the optimization to apply and show that these conditions are strictly connected with the presence of functional dependencies between the attributes involved in the queries. We show some experiments on an initial prototype of an optimizer which demonstrates that this approach to query answering is viable and in many practical cases it drastically reduces the query execution time.     

Efficient query expansion with auxiliary data structures

Query expansion is a well-known method for improving average effectiveness in information retrieval. The most effective query expansion methods rely on retrieving documents which are used as a source of expansion terms. Retrieving those documents is costly. We examine the bottlenecks of a conventional approach and investigate alternative methods aimed at reducing query evaluation time. We propose a new method that draws candidate terms from brief document summaries that are held in memory for each document. While approximately maintaining the effectiveness of the conventional approach, this method significantly reduces the time required for query expansion by a factor of 5–10.