Term Rewriting and All That
From MaRDI portal
Publication:4702972
DOI10.1017/CBO9781139172752zbMath0948.68098MaRDI QIDQ4702972
Publication date: 13 December 1999
08A70: Applications of universal algebra in computer science
03B35: Mechanization of proofs and logical operations
68-02: Research exposition (monographs, survey articles) pertaining to computer science
68Q42: Grammars and rewriting systems
Related Items
Polynomials over the reals in proofs of termination : from theory to practice, Cadmium: An Implementation of ACD Term Rewriting, The narrowing-driven approach to functional logic program specialization, Model-theoretic methods in combined constraint satisfiability, On the complexity of deduction modulo leaf permutative equations, Reachability analysis over term rewriting systems, Mechanically proving termination using polynomial interpretations, Ordinal arithmetic: Algorithms and mechanization, Cones and foci: A mechanical framework for protocol verification, An effective proof of the well-foundedness of the multiset path ordering, Tool-assisted specification and verification of typed low-level languages, Formal correctness of a quadratic unification algorithm, Elimination transformations for associative-commutative rewriting systems, Mechanizing and improving dependency pairs, The disconnection tableau calculus, A new generic scheme for functional logic programming with constraints, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., Loop detection in term rewriting using the eliminating unfoldings, Adding constants to string rewriting, Deciding the word problem in the union of equational theories., Decidability for left-linear growing term rewriting systems., Theorem proving modulo, Equational rules for rewriting logic, Constraint solving for proof planning, Relative undecidability in term rewriting. I: The termination hierarchy, Relative undecidability in term rewriting. II: The confluence hierarchy, Context-sensitive rewriting strategies, A graphical user interface for formal proofs in geometry, Reasoning in description logics by a reduction to disjunctive datalog, Confluence theory for graphs, Expression reduction systems with patterns, Constructing invariants for hybrid systems, The three dimensions of proofs, The size-change principle and dependency pairs for termination of term rewriting, A structural approach to reversible computation, Structures for abstract rewriting, General \(E\)-unification with eager variable elimination and a nice cycle rule, Theories of orders on the set of words, A CORRESPONDENCE BETWEEN BALANCED VARIETIES AND INVERSE MONOIDS, ALGORITHMIC PROBLEMS ON INVERSE MONOIDS OVER VIRTUALLY FREE GROUPS, EVANS' NORMAL FORM THEOREM REVISITED, Theory of finite or infinite trees revisited, An insertion operator preserving infinite reduction sequences, Safety of Nöcker's strictness analysis, Deciding Innermost Loops, Certifying a Termination Criterion Based on Graphs, without Graphs, Using groups for investigating rewrite systems, Building language towers with Ziggurat, From Outermost Termination to Innermost Termination, First-class patterns, Welcome to Constraint Handling Rules, A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs
Uses Software
