Counterexamples in infinitary rewriting with non-fully-extended rules

We show counterexamples exist to confluence modulo hypercollapsing subterms, fair normalisation, and the normal form property in orthogonal infinitary higher-order rewriting with non-fully-extended rules. This sets these systems apart from both fully-extended and finite systems, where no such counterexamples are possible.     

A Higher-Order Calculus for Graph Transformation

This paper presents a formalism for defining higher-order systems based on the notion of graph transformation (by rewriting or interaction). The syntax is inspired by the Combinatory Reduction Systems of Klop. The rewrite rules can be used to define first-order systems, such as graph or term-graph rewriting systems, Lafont's interaction nets, the interaction systems of Asperti and Laneve, the non-deterministic nets of Alexiev, or a process calculus. They can also be used to specify higher-order systems such as hierarchical graphs and proof nets of Linear Logic, or to specify the operational semantics of graph-based languages.     

Expression Reduction Systems with Patterns

We introduce a new higher-order rewriting formalism, called expression reduction systems with patterns (ERSP), where abstraction is allowed not only on variables but also on nested patterns with metavariables. These patterns are built by combining standard algebraic patterns with choice constructors denoting cases. In other words, the nondeterministic choice between different rewrite rules which is inherent to classical rewriting formalisms can be lifted here to the level of patterns. We show that confluence holds for a reasonable class of systems and terms.     

On confluence and residuals in Cauchy convergent transfinite rewriting

We show that non-collapsing orthogonal term rewriting systems do not have the transfinite Church-Rosser property in the setting of Cauchy convergence. In addition, we show that for (a transfinite version of) the Parallel Moves Lemma to hold, any definition of residual for Cauchy convergent rewriting must either part with a number of fundamental properties enjoyed by rewriting systems in the finitary and strongly convergent settings, or fail to hold for very simple rewriting systems.     

Completion for Multiple Reduction Orderings

We present a completion procedure (called MKB) that works for multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structures consisting of a pair s : t of terms associated with the information to show which processes contain the rule s t (or t s) and which processes contain the equation s t. The idea is based on the observation that some inferences made in different processes are often closely related, so we can design inference rules that simulate these inferences all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough. We also present an extension of this technique to the unfailing completion for multiple reduction orderings, which is useful in various areas of automated reasoning, including equational theorem proving.     

基于Anytime算法的组合优化问题求解

介绍一种基于Ａｎｙｔｉｍｅ算法的组合优化问题求解框架,并报告了对ＴＳＰ问题进行求解的实验。实验结果表明,上述框架可以较好地协调２的复杂度与求解时间要求之间的冲突。     

汉语组合类型语法

组合类型语法是从计算机处理汉语的角度, 在范畴语法的基拙上提出的一种汉语的形式语法理论。本文介绍了其基本思想及所建立的汉语语法体系, 并给出了一些描述实例。     

Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions

The paper presents three formal proving methods for generalized weakly ground terminating property, i.e., weakly terminating property in a restricted domain of a term rewriting system, one with structural induction, one with cover-set induction, and the third without induction, and describes their mechanization based on a meta-computation model for term rewriting systems-dynamic term rewriting calculus. The methods can be applied to non-terminating, non-confluent and/or non-left-linear term rewriting systems. They can do "forward proving" by applying propositions in the proof, as well as "backward proving" by discovering lemmas during the proof.     

组合分析蚀变信息提取方法研究

目前主成分分析法、比值法、光谱角制图法等已广泛应用于遥感矿化蚀变信息提取中,且取得了很好的效果。根据研究区遥感数据特点,采用比值与主成分组合分析的方法,结合FLAASH大气校正、中值滤波以及彩色密度分割等图像处理方法,对新疆且末地区ASTER数据进行蚀变信息提取。经USGS标准矿物波谱库中典型矿物光谱的验证,组合分析方法能够去除数据冗余和噪声,有利于各类蚀变信息的提取。     

直、摆组合凸轮机构动态仿真技术研究

直、摆组合凸轮机构是一种新型的机构类型，它所能实现的凸轮曲线非常丰富多彩，对其进行运动仿真，对于验证设计的正确性以及指导实际生产都有重要的现实意义。该文首先简介了直、摆组合凸轮机构的设计方法，进而介绍了该机构的动态仿真软件和动态仿真技术，并对动态仿真中的几点关键技术作了进一步的阐述。     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

Reachability Analysis over Term Rewriting Systems

This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by . An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.     

不完备信息系统的属性约简算法研究

对基于容差关系的属性约简进行研究,提出了一种属性次序下的基于容差关系的属性约简算法。在给定属性次序的条件下,该算法可以计算不完备信息系统的惟一约简。通过典型实例验证了该算法的有效性和可行性。     

A rewriting approach to binary decision diagrams

Binary decision diagrams (BDDs) provide an established technique for propositional formula manipulation. In this paper, we present the basic BDD theory by means of standard rewriting techniques. Since a BDD is a DAG instead of a tree we need a notion of shared rewriting and develop appropriate theory. A rewriting system is presented by which canonical reduced ordered BDDs (ROBDDs) can be obtained and for which uniqueness of ROBDD representation is proved. Next, an alternative rewriting system is presented, suitable for actually computing ROBDDs from formulas. For this rewriting system a layerwise strategy is defined, and it is proved that when replacing the classical apply-algorithm by layerwise rewriting, roughly the same complexity bound is reached as in the classical algorithm. Moreover, a layerwise innermost strategy is defined and it is proved that the full classical algorithm for computing ROBDDs can be replaced by layerwise innermost rewriting without essentially affecting the complexity. Finally a lazy strategy is proposed sometimes performing much better than the traditional algorithm.     

Paramodulation and Knuth–Bendix Completion with Nontotal and Nonmonotonic Orderings

Up to now, all existing completeness results for ordered paramodulation and Knuth–Bendix completion have required term ordering to be well founded, monotonic, and total(izable) on ground terms. For several applications, these requirements are too strong, and hence weakening them has been a well-known research challenge.Here we introduce a new completeness proof technique for ordered paramodulation where the only properties required on are well-foundedness and the subterm property. The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS).By a careful further analysis of our technique, we obtain the first Knuth–Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering whenever it exists. Note that being a reduction ordering is the minimal possible requirement on , since a TRS terminates if, and only if, it is contained in a reduction ordering.     

依赖项重写系统及其在程序设计语言中的应用

面重写系统是一种简洁通用的计算模型，在许多领域中有着重要的应用。     

Practical ultra‐reliability for abstract data types

The Term Redundancy Method (TRM) is a novel approach for obtaining ultra‐reliable programs through specification‐based testing. Current specification‐based testing schemes need a prohibitively large number of test cases for estimating ultra‐reliability. They assume the availability of an accurate program‐usage distribution prior to testing, and they assume the availability of a test oracle. This paper shows how to obtain ultra‐reliable abstract data types specified with equational specifications, with a practical number of test cases, without an accurate usage distribution, and without the usual test oracle. The effectiveness of the TRM in failure detection and recovery is demonstrated on the aircraft collision avoidance system TCAS. Copyright © 2007 John Wiley & Sons, Ltd.     

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.