共查询到20条相似文献,搜索用时 15 毫秒
1.
Jeroen Ketema 《Information Processing Letters》2011,111(13):642-646
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. 相似文献
2.
Maribel Fernndez Ian Mackie Jorge Sousa Pinto 《Electronic Notes in Theoretical Computer Science》2007,72(1):45
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. 相似文献
3.
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. 相似文献
4.
Jakob Grue Simonsen 《Information Processing Letters》2004,91(3):141-146
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. 相似文献
5.
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. 相似文献
6.
7.
8.
9.
Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions
下载免费PDF全文
![点击此处可从《计算机科学技术学报》网站下载免费的PDF全文](/ch/ext_images/free.gif)
Su Feng 《计算机科学技术学报》2005,20(4):496-513
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. 相似文献
10.
11.
12.
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. 相似文献
13.
Guillaume Feuillade Thomas Genet Valérie Viet Triem Tong 《Journal of Automated Reasoning》2004,33(3-4):341-383
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. 相似文献
14.
15.
对基于容差关系的属性约简进行研究,提出了一种属性次序下的基于容差关系的属性约简算法。在给定属性次序的条件下,该算法可以计算不完备信息系统的惟一约简。通过典型实例验证了该算法的有效性和可行性。 相似文献
16.
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. 相似文献
17.
Miquel Bofill Guillem Godoy Robert Nieuwenhuis Albert Rubio 《Journal of Automated Reasoning》2003,30(1):99-120
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. 相似文献
18.
19.
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. 相似文献
20.
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. 相似文献