scientific article; zbMATH DE number 1142316
From MaRDI portal
Publication:4385532
zbMath0900.68283MaRDI QIDQ4385532
Nachum Dershowitz, Jean-Pierre Jouannaud
Publication date: 14 May 1998
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (only showing first 100 items - show all)
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
This page was built for publication:
