scientific article; zbMATH DE number 1142316

zbMath0900.68283MaRDI QIDQ4385532

Nachum Dershowitz, Jean-Pierre Jouannaud

Publication date: 14 May 1998

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Bottom-up tree pushdown automata: Classification and connection with rewrite systems, Strongly sequential and inductively sequential term rewriting systems, Extending reduction orderings to ACU-compatible reduction orderings, Algebraic simulations, Termination of rewriting, Mechanically proving termination using polynomial interpretations, Proving termination of context-sensitive rewriting by transformation, An undecidability result for AGh, Paramodulation with non-monotonic orderings and simplification, Intruder deduction for the equational theory of abelian groups with distributive encryption, A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux, Higher-order rewrite systems and their confluence, Bubbles in modularity, A polynomial algorithm testing partial confluence of basic semi-Thue systems, A new generic scheme for functional logic programming with constraints, Linear generalized semi-monadic rewrite systems effectively preserve recognizability, Derived semidistributive lattices, The two-way rewriting in action: removing the mystery of Euler-Glaisher's map, Equational unification, word unification, and 2nd-order equational unification, Tree algebras and varieties of tree languages, Semantic types and approximation for Featherweight Java, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Sufficient completeness verification for conditional and constrained TRS, Decidability and combination results for two notions of knowledge in security protocols, Some classes of term rewriting systems inferable from positive data, Developments from enquiries into the learnability of the pattern languages from positive data, A formal library of set relations and its application to synchronous languages, Rewrite, rewrite, rewrite, rewrite, rewrite, \dots, Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations, A framework for the verification of infinite-state graph transformation systems, Semantics of order-sorted specifications, Sequentiality in orthogonal term rewriting systems, Basic notions of universal algebra for language theory and graph grammars, A sequential reduction strategy, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, A compositional semantic basis for the analysis of equational Horn programs, Lazy narrowing: strong completeness and eager variable elimination, Intersection type assignment systems with higher-order algebraic rewriting, Using induction and rewriting to verify and complete parameterized specifications, Partial derivatives of regular expressions and finite automaton constructions, Transformations and confluence for rewrite systems, Infinite normal forms for non-linear term rewriting systems, Modular termination of \(r\)-consistent and left-linear term rewriting systems, Towards a foundation of completion procedures as semidecision procedures, Modularity in noncopying term rewriting, Equational abstractions, Term rewriting and Hoare logic -- Coded rewriting, Natural termination, Some undecidable termination problems for semi-Thue systems, Rewriting extended regular expressions, A combinatory logic approach to higher-order E-unification, Deciding observational congruence of finite-state CCS expressions by rewriting, Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Termination is not modular for confluent variable-preserving term rewriting systems, Conditional rewriting logic as a unified model of concurrency, Groups with a complemented presentation, Strict coherence of conditional rewriting modulo axioms, Narrowing based procedures for equational disunification, Using geometric rewrite rules for solving geometric problems symbolically, Complete axiomatizations of some quotient term algebras, On the complexity of recursive path orderings, Modularity of simple termination of term rewriting systems with shared constructors, Simulation of Turing machines by a regular rewrite rule, Termination and completion modulo associativity, commutativity and identity, Termination proofs by multiset path orderings imply primitive recursive derivation lengths, An improved general \(E\)-unification method, A field guide to equational logic, C-expressions: A variable-free calculus for equational logic programming, Well rewrite orderings and well quasi-orderings, A new method for undecidability proofs of first order theories, Quasi-interpretations. A way to control resources, Programming with narrowing: a tutorial, Equational approximations for tree automata completion, On the confluence of lambda-calculus with conditional rewriting, A compact fixpoint semantics for term rewriting systems, Type-based homeomorphic embedding for online termination, The Hydra battle and Cichon's principle, Linearizing well quasi-orders and bounding the length of bad sequences, From a zoo to a zoology: Towards a general theory of graph polynomials, How to win a game with features, Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering, Modular aspects of term graph rewriting, Semantics and strong sequentiality of priority term rewriting systems, Superposition theorem proving for abelian groups represented as integer modules, The first-order theory of linear one-step rewriting is undecidable, Orders, reduction graphs and spectra, Decidability and complexity analysis by basic paramodulation, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Termination of narrowing revisited, Combination of convex theories: modularity, deduction completeness, and explanation, Some results on cut-elimination, provable well-orderings, induction and reflection, Constructing inverse semigroups from category actions, Regular path queries with constraints, Combinatory reduction systems: Introduction and survey, Modularity of confluence: A simplified proof, Automated proofs of equality problems in Overbeek's competition, Competing for the \(AC\)-unification race, Deductive and inductive synthesis of equational programs, Algebraic specification of agent computation, Proving termination of (conditional) rewrite systems. A semantic approach, Context rewriting, Consistency and semantics of equational definitions over predefined algebras, Collapsed tree rewriting: Completeness, confluence, and modularity, Revisiting Semantics of Interactions for Trace Validity Analysis, Associative-commutative discrimination nets, About the theory of tree embedding, Term rewriting in CTΣ, On μ-symmetric polynomials, Time bounded rewrite systems and termination proofs by generalized embedding, Narrowing directed by a graph of terms, Decidability of confluence and termination of monadic term rewriting systems, On fairness of completion-based theorem proving strategies, Proving equational and inductive theorems by completion and embedding techniques, On proving properties of completion strategies, Open problems in rewriting, Bi-rewriting, a term rewriting technique for monotonic order relations, Distributing equational theorem proving, Improving transformation systems for general E-unification, Some lambda calculi with categorical sums and products, Optimal normalization in orthogonal term rewriting systems, More problems in rewriting, Automatic termination proofs with transformation orderings, On narrowing, refutation proofs and constraints, Concurrent garbage collection for concurrent rewriting, Lazy rewriting and eager machinery, Level-confluence of conditional rewrite systems with extra variables in right-hand sides, Relating two categorical models of term rewriting, (Head-)normalization of typeable rewrite systems, Explicit substitutions with de bruijn's levels, Some independence results for equational unification, Generating polynomial orderings for termination proofs, Problems in rewriting III, Fine-grained concurrent completion, Termination of constructor systems, Dummy elimination in equational rewriting, On proving termination by innermost termination, A recursive path ordering for higher-order terms in η-long β-normal form, Modularity of termination in term graph rewriting, Confluence of terminating conditional rewrite systems revisited, The first-order theory of one-step rewriting is undecidable, On the termination problem for one-rule semi-Thue system, Decidable approximations of term rewriting systems, Semantics and strong sequentially of priority term rewriting systems, Higher-order families, Rewriting regular inequalities, Dummy elimination: Making termination easier, Unique normal forms for nonlinear term rewriting systems: Root overlaps, String Diagram Rewrite Theory I: Rewriting with Frobenius Structure, Buchberger's algorithm: The term rewriter's point of view, Equation solving in conditional AC-theories, An abstract concurrent machine for rewriting, Jungle rewriting: An abstract description of a lazy narrowing machine, A confluent relational calculus for higher-order programming with constraints, “Syntactic” AC-unification, On modularity in term rewriting and narrowing, Higher order conditional rewriting and narrowing, Buchberger's algorithm: A constraint-based completion procedure, An introduction to category-based equational logic, CPO models for infinite term rewriting, Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems, Lazy narrowing: Strong completeness and eager variable elimination (extended abstract), Negation elimination in equational formulae, One-rule trace-rewriting systems and confluence, Rational rewriting, Critical pairs in term graph rewriting, Well-founded coalgebras, revisited, Unnamed Item, Unnamed Item, Proving convergence of self-stabilizing systems using first-order rewriting and regular languages, Confluence: The Unifying, Expressive Power of Locality, Functional Logic Programming: From Theory to Curry, FLIC: Application to Caching of a Dynamic Dependency Analysis for a 3D Oriented CRS, A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, Closure of Tree Automata Languages under Innermost Rewriting, AC complement problems: Satisfiability and negation elimination, Variant Narrowing and Equational Unification, A polynomial algorithm testing partial confluence of basic semi-Thue systems, Superposition theorem proving for abelian groups represented as integer modules, Simple termination is difficult, Any ground associative-commutative theory has a finite canonical system, On Transfinite Knuth-Bendix Orders, Completion of rewrite systems with membership constraints, Completion for multiple reduction orderings, Induction using term orderings, On notions of inductive validity for first-order equational clauses, Simple termination revisited, Termination orderings for rippling, Associative-commutative deduction with constraints, AC-superposition with constraints: No AC-unifiers needed, On pot, pans and pudding or how to discover generalised critical Pairs, Total termination of term rewriting, Completeness of combinations of constructor systems, Termination proofs by multiset path orderings imply primitive recursive derivation lengths, How to win a game with features, Decidable call by need computations in term rewriting (extended abstract), A Set-theoretic Approach to Reasoning Services for the Description Logic 𝒟 ℒ D 4,×, ON THE INVARIANCE OF GÖDEL’S SECOND THEOREM WITH REGARD TO NUMBERINGS, Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation, Towards an Efficient Implementation of Tree Automata Completion, Termination by absence of infinite chains of dependency pairs, Decidability of reachability for disjoint union of term rewriting systems, Abduction in logic programming: A new definition and an abductive procedure based on rewriting, Generalized sufficient conditions for modular termination of rewriting, Completeness results for basic narrowing, Finding direct partition bijections by two-directional rewriting techniques, Pattern matching as cut elimination, Sound generalizations in mathematical induction, On subsumption in distributed derivations, Right-linear half-monadic term rewrite systems, Ground reducibility is EXPTIME-complete, A complete equational axiomatization for prefix iteration, Simple termination is difficult, Implicit induction in conditional theories, On the modularity of termination of term rewriting systems, Combining algebraic rewriting, extensional lambda calculi, and fixpoints, Modular proofs for completeness of hierarchical term rewriting systems, Buchberger's algorithm: The term rewriter's point of view, Proving Ramsey's theory by the cover set induction: A case and comparision study., Asynchronous communication model based on linear logic, Normalization results for typeable rewrite systems, Category-based modularisation for equational logic programming, Normal forms in combinatory logic, Incremental constraint satisfaction for equational logic programming, Total termination of term rewriting, Induction using term orders, Unification in sort theories and its applications, Lambda calculus with explicit recursion, On the rational subsets of the free group, From diagrammatic confluence to modularity, Interaction nets and term-rewriting systems, Some general results about proof normalization, Abstract data type systems, Proof systems for structured specifications with observability operators, Simple termination of rewrite systems, Developing developments, The first-order theory of lexicographic path orderings is undecidable, Unification of infinite sets of terms schematized by primal grammars, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Declarative debugging of rewriting logic specifications, Linguistic\(\leftrightarrow \)rational agents' semantics, Practical algorithms for deciding path ordering constraint satisfaction., A characterisation of multiply recursive functions with Higman's lemma., A linear logical framework, On the transition graphs of Turing machines., A rewriting approach to satisfiability procedures., The unification problem for confluent right-ground term rewriting systems., Analysing the implicit complexity of programs., An upper bound on the derivational complexity of Knuth-Bendix orderings., Proof theory of higher-order equations: Conservativity, normal forms and term rewriting., Constraint contextual rewriting., Intersection of the reflexive transitive closures of two rewrite relations induced by term rewriting systems, Monadic simultaneous rigid \(E\)-unification, Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach, Theorem proving modulo, Superposition with completely built-in abelian groups, Elimination of conditions, Proving theorems by reuse, Specification and proof in membership equational logic, Termination of term rewriting using dependency pairs, Logicality of conditional rewrite systems, Remarks on Thatte's transformation of term rewriting systems, Decision problems for semi-Thue systems with a few rules, A procedure for deciding symbolic equivalence between sets of constraint systems, Normalisation for higher-order calculi with explicit substitutions, Tree automata with one memory set constraints and cryptographic protocols, Abstract interpretation of mobile systems, Loop checking in SLD-derivations by well-quasi-ordering of goals, Pattern-matching algorithms based on term rewrite systems, Some characteristics of strong innermost normalization, A property of left-linear rewrite systems preserving recognizability, Decidability and complexity of simultaneous rigid E-unification with one variable and related results, Rational languages defined with a non-associative concatenation, MV-algebras, multiple bets and subjective states, Skew confluence and the lambda calculus with letrec, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Propositional compositions of partial predicates, Partial completion of equational theories, Algorithms and reductions for rewriting problems. II., Unions of non-disjoint theories and combinations of satisfiability procedures, Normalization, approximation, and semantics for combinator systems, Logic with equality: Partisan corroboration and shifted pairing, Bisimilarity in term graph rewriting., Sequentiality, monadic second-order logic and tree automata., Higher order unification via explicit substitutions, Descendants and origins in term rewriting., Induction = I-axiomatization + first-order consistency., Complexity of nilpotent unification and matching problems., On terminating lemma speculations., Using tableaux to automate the Lambek and other categorial calculi, Automata-driven automated induction, A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser, The undecidability of the first-order theories of one step rewriting in linear canonical systems, Set of support, demodulation, paramodulation: a historical perspective, A hidden Herbrand theorem: Combining the object and logic paradigms, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), A unified language processing methodology, Cancellative Abelian monoids and related structures in refutational theorem proving. I, ELAN from a rewriting logic point of view, Maude: specification and programming in rewriting logic, Reflection in conditional rewriting logic, Web ontology representation and reasoning via fragments of set theory, Some decidable congruences of free monoids, A graphical representation of relational formulae with complementation, Closure properties of linear context-free tree languages with an application to optimality theory, Nominal rewriting, Garside and Quadratic Normalisation: A Survey, LARS: a learning algorithm for rewriting systems, Structures for abstract rewriting, Modular and incremental proofs of AC-termination, On confluence and residuals in Cauchy convergent transfinite rewriting, On explicit substitution with names, Monadic simultaneous rigid E-unification and related problems, On modular properties of higher order extensional lambda calculi, The word matching problem is undecidable for finite special string-rewriting systems that are confluent, The theory of vaccines, Nominal syntax with atom substitutions, Size-based termination of higher-order rewriting, Implementing term rewriting by jungle evaluation, On confluence of one-rule trace-rewriting systems, On confluence versus strong confluence for one-rule trace-rewriting systems, A Structural Theory of Rhythm Notation Based on Tree Representations and Term Rewriting, Metalevel algorithms for variant satisfiability, On First-Order Model-Based Reasoning, Normal Higher-Order Termination, A Probabilistic Applied Pi–Calculus, Verifying Cryptographic Protocols with Subterms Constraints, Drags: a compositional algebraic framework for graph rewriting, Unification of drags and confluence of drag rewriting, Tree automata with equality constraints modulo equational theories, Efficient theory combination via Boolean search, Modular Termination of Basic Narrowing, Growth of positive words and lower bounds of the growth rate for Thompson’s groups F(p), Canonical Inference for Implicational Systems, Automated Induction with Constrained Tree Automata, Unnamed Item, Certifying a Termination Criterion Based on Graphs, without Graphs, Multiset rewriting over Fibonacci and tribonacci numbers, A partial solution for D-unification based on a reduction to AC 1-unification, Pumping, cleaning and symbolic constraints solving, Dynamically-typed computations for order-sorted equational presentations, A reconstruction and extension of Maple's assume facility via constraint contextual rewriting, A survey of strategies in rule-based program transformation systems, Evaluation strategies for functional logic programming, Decidability of bounded higher-order unification, E-generalization using grammars, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, Unnamed Item, Up-To Techniques for Weighted Systems, What Is Essential Unification?, Compositional synthesis of maximally permissive supervisors using supervision equivalence, Extension orderings, Approximation and normalization results for typeable term rewriting systems, Collapsing partial combinatory algebras, Development closed critical pairs, Termination of theorem proving by reuse, Unification and matching modulo nilpotence, Unification in pseudo-linear sort theories is decidable, Transforming termination by self-labelling, Theorem proving in cancellative abelian monoids (extended abstract), Rewrite semantics for production rule systems: Theory and applications, Walther recursion, Grammar specification in categorial logics and theorem proving, Canonical Ground Horn Theories, A Computation of the Maximal Order Type of the Term Ordering on Finite Multisets, Symbolic protocol analysis for monoidal equational theories, Hierarchical combination of intruder theories, Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures, Essential unifiers, On modularity in infinitary term rewriting, Ensuring termination by typability, Variant-Based Satisfiability in Initial Algebras, Reasoning on Schemas of Formulas: An Automata-Based Approach, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, A partial evaluation framework for order-sorted equational programs modulo axioms, Ground confluence of order-sorted conditional specifications modulo axioms, Shallow confluence of conditional term rewriting systems, Order-Sorted Rewriting and Congruence Closure, Confluence by critical pair analysis revisited, Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions, The Inclusion Problem of Context-Free Languages: Some Tractable Cases, TAGED Approximations for Temporal Properties Model-Checking, Metalevel Algorithms for Variant Satisfiability, HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA, Unnamed Item, Conditions for confluence of innermost terminating term rewriting systems, Evaluation Strategies for Functional Logic Programming, Declarative Debugging of Functional Logic Programs1 1This work has been partially supported by CICYT under grant TIC2001-2705-C03-01, by Accóon Integrada Hispano-Italiana HI2000-0161 and by Generalitat Valenciana under grant GV01-424., Compact Normalisation Trace via Lazy Rewriting, A Survey of Rewriting Strategies in Program Transformation Systems, Induction for termination with local strategies, Knuth-Bendix Completion for Non-Symmetric Transitive Relations, Timed Term Rewrite Systems, Defining Actions in Concurrent Declarative Programming, More efficient left-to-right matching for overlapping pattern, Decidable first-order transition logics for PA-processes, A structural approach to reversible computation, An Account of Implementing Applicative Term Rewriting, Lazy Context Cloning for Non-Deterministic Graph Rewriting, SMELS: satisfiability modulo equality with lazy superposition, Combinations of simplifying conditional term rewriting systems, Termination of term rewriting by interpretation, Path orderings for termination of associative-commutative rewriting, Generic induction proofs, Reduction techniques for first-order reasoning, Semigroups satisfying x m+n = x n, Could orders be captured by term rewriting systems?, A categorical formulation for critical-pair/completion procedures, Implementing contextual rewriting, Confluence of terminating membership conditional TRS, Termination proofs of well-moded logic programs via conditional rewrite systems, Normalization by leftmost innermost rewriting, A strategy to deal with divergent rewrite systems, A new approach to general E-unification based on conditional rewriting systems, Extended term rewriting systems, Conditional rewriting logic: Deduction, models and concurrency, Higher-order unification, polymorphism, and subsorts, A modular construction of type theories, The next 700 program transformers, Rewriting logic as a semantic framework for concurrency: a progress report, Variants and satisfiability in the infinitary unification wonderland, A note on confluent Thue systems, A simple language supporting angelic nondeterminism and parallel composition, Local confluence of conditional and generalized term rewriting systems, Positive Plücker tree certificates for non-realizability, Strictly orthogonal left linear rewrite systems and primitive recursion, Normal forms for connectedness in categories, Regular database update logics, On interreduction of semi-complete term rewriting systems, Solving the word problem for two classes of non-associative rings by rewriting, The control layer in open mechanized reasoning systems: Annotations and tactics, Implementing conditional term rewriting by graph rewriting, Inductive-data-type systems, On the longest perpetual reductions in orthogonal expression reduction systems