Term Rewriting and All That
From MaRDI portal
Publication:4702972
DOI10.1017/CBO9781139172752zbMath0948.68098OpenAlexW4230919050MaRDI QIDQ4702972
Publication date: 13 December 1999
Full work available at URL: https://doi.org/10.1017/cbo9781139172752
Applications of universal algebra in computer science (08A70) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Grammars and rewriting systems (68Q42)
Related Items
Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Pumping for ordinal-automatic structures1 ⋮ Unnamed Item ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ Demand-Driven Normalisation for ACD Term Rewriting ⋮ Thompson-like groups, Reidemeister numbers, and fixed points ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Order Reconfiguration under Width Constraints ⋮ Arkhipov's theorem, graph minors, and linear system nonlocal games ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting ⋮ The Maude strategy language ⋮ Free weighted (modified) differential algebras, free (modified) Rota–Baxter algebras and Gröbner–Shirshov bases ⋮ Equational Theorem Proving for Clauses over Strings ⋮ Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ A Comparison of Sets of Recognizable Weighted Tree Languages Over Specific Sets of Bounded Lattices ⋮ Rewriting system of certain semigroups with three generators ⋮ Analysing parallel complexity of term rewriting ⋮ Unnamed Item ⋮ Inverse Unfold Problem and Its Heuristic Solving ⋮ Probabilistic logic over equations and domain restrictions ⋮ On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings ⋮ Towards Modelling Actor-Based Concurrency in Term Rewriting ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ a-Logic With Arrows ⋮ Singular and plural functions for functional logic programming ⋮ Clocks for Functional Programs ⋮ CONSTRUCTION OF FREE COMMUTATIVE INTEGRO-DIFFERENTIAL ALGEBRAS BY THE METHOD OF GRÖBNER–SHIRSHOV BASES ⋮ Analogy in Automated Deduction: A Survey ⋮ A Type-Theoretic Approach to Resolution ⋮ A Typed Language for Events ⋮ An automated approach to the Collatz conjecture ⋮ An Extension of Complex Role Inclusion Axioms in the Description Logic $\mathcal{SROIQ}$ ⋮ The narrowing-driven approach to functional logic program specialization ⋮ Properties of certain semigroups and their potential as platforms for cryptosystems ⋮ Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems ⋮ Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems ⋮ The HOM Problem is EXPTIME-Complete ⋮ Cut Elimination, Substitution and Normalisation ⋮ Automated Verification of Equivalence Properties of Cryptographic Protocols ⋮ Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic Programs ⋮ The Derivational Complexity Induced by the Dependency Pair Method ⋮ Characterizing Compatible View Updates in Syntactic Bidirectionalization ⋮ Rewriting systems and biautomatic structures for Chinese, hypoplactic, and sylvester monoids ⋮ Cadmium: An Implementation of ACD Term Rewriting ⋮ SAT-Inspired Eliminations for Superposition ⋮ Rewriting in Gray categories with applications to coherence ⋮ A proof method for local sufficient completeness of term rewriting systems ⋮ Relative termination via dependency pairs ⋮ Confluence of orthogonal term rewriting systems in the prototype verification system ⋮ Sharing in the Graph Rewriting Calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Short Introduction to Implicit Computational Complexity ⋮ Unnamed Item ⋮ Operational semantics of resolution and productivity in Horn clause logic ⋮ MetaFEM: a generic FEM solver by meta-expressions ⋮ Extended feature algebra ⋮ Tree Transformations and Dependencies ⋮ A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints ⋮ Towards finding longer proofs ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ Moving the bar on computationally sound exclusive-or ⋮ Analogical proportions ⋮ Structures for abstract rewriting ⋮ General \(E\)-unification with eager variable elimination and a nice cycle rule ⋮ Hopf algebra of multidecorated rooted forests, free matching Rota-Baxter algebras and Gröbner-Shirshov bases ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ On explicit substitution with names ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Reduction operators and completion of rewriting systems ⋮ Schematic refutations of formula schemata ⋮ Alice and Bob Meet Equational Theories ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ Layer Systems for Proving Confluence ⋮ An Equation-Based Classical Logic ⋮ Resolution with order and selection for hybrid logics ⋮ A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings ⋮ Formalizing Soundness and Completeness of Unravelings ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ Unification and Matching in Hierarchical Combinations of Syntactic Theories ⋮ Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification ⋮ GROWTHS OF ENDOMORPHISMS OF FINITELY GENERATED SEMIGROUPS ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ A formal language for cyclic operads ⋮ Canonized Rewriting and Ground AC Completion Modulo Shostak Theories ⋮ Commutative rational term rewriting ⋮ The spirit of node replication ⋮ Certifying proofs in the first-order theory of rewriting ⋮ An Access Control Language Based on Term Rewriting and Description Logic ⋮ A graphical user interface for formal proofs in geometry ⋮ Reasoning in description logics by a reduction to disjunctive datalog ⋮ Confluence theory for graphs ⋮ Parallel coherent graph transformations ⋮ Expression reduction systems with patterns ⋮ Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems ⋮ Rewriting in Varieties of Idempotent Semigroups ⋮ Constructing invariants for hybrid systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Convergent presentations and polygraphic resolutions of associative algebras ⋮ The three dimensions of proofs ⋮ Compilation of static and evolving conditional knowledge bases for computing induced nonmonotonic inference relations ⋮ Fault-Tolerant Aggregate Signatures ⋮ Reasoning on Schemas of Formulas: An Automata-Based Approach ⋮ Rule-Based Modeling of Transcriptional Attenuation at the Tryptophan Operon ⋮ Decision Procedures for Automating Termination Proofs ⋮ Topological rewriting systems applied to standard bases and syntactic algebras ⋮ Unary Resolution: Characterizing Ptime ⋮ Nominal Confluence Tool ⋮ On the correctness of pull-tabbing ⋮ Analysing graph transformation systems through constraint handling rules ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ Unification modulo lists with reverse relation with certain word equations ⋮ Restricted combinatory unification ⋮ Model completeness, covers and superposition ⋮ Confluence by critical pair analysis revisited ⋮ Composing proof terms ⋮ Certified equational reasoning via ordered completion ⋮ Survey: Weighted Extended Top-Down Tree Transducers Part III — Composition ⋮ Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems ⋮ Automated Certification of Implicit Induction Proofs ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ The number of clones determined by disjunctions of unary relations ⋮ Set-blocked clause and extended set-blocked clause in first-order logic ⋮ Function simulation, graph grammars and colourings ⋮ The size-change principle and dependency pairs for termination of term rewriting ⋮ Polygraphs of finite derivation type ⋮ The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics ⋮ Similarity issues of confluence of fuzzy relations ⋮ A structural approach to reversible computation ⋮ Rewrite-Based Satisfiability Procedures for Recursive Data Structures ⋮ Tuple interpretations for termination of term rewriting ⋮ Inductive theorem proving based on tree grammars ⋮ Fast left Kan extensions using the chase ⋮ Ground joinability and connectedness in the superposition calculus ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ A framework for approximate generalization in quantitative theories ⋮ From Hertzsprung's problem to pattern-rewriting systems ⋮ Analyzing innermost runtime complexity of term rewriting by dependency pairs ⋮ Non-linear rewrite closure and weak normalization ⋮ Emptiness and finiteness for tree automata with global reflexive disequality constraints ⋮ Labelings for decreasing diagrams ⋮ Runtime complexity analysis of logically constrained rewriting ⋮ Pattern eliminating transformations ⋮ Terminating non-disjoint combined unification ⋮ Effective codescent morphisms in the varieties determined by convergent term rewriting systems. ⋮ Non-disjoint combined unification and closure by equational paramodulation ⋮ Loop detection by logically constrained term rewriting ⋮ Algorithms for Kleene algebra with converse ⋮ Crystal monoids \& crystal bases: rewriting systems and biautomatic structures for plactic monoids of types \(A_{n}\), \(B_{n}\), \(C_{n}\), \(D_{n}\), and \(G_{2}\) ⋮ Decision problems for word-hyperbolic semigroups ⋮ The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem ⋮ Coq formalization of the higher-order recursive path ordering ⋮ KBO orientability ⋮ 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 ⋮ Geometric and combinatorial views on asynchronous computability ⋮ Uncurrying for termination and complexity ⋮ Paramodulation with non-monotonic orderings and simplification ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ Formalization of the resolution calculus for first-order logic ⋮ 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 ⋮ Rewriting systems over similarity and generalized pseudometric spaces and their properties ⋮ On unification and admissible rules in Gabbay-de Jongh logics ⋮ Simulation relations for pattern matching in directed graphs ⋮ Some general results about proof normalization ⋮ A formalization of the Knuth-Bendix(-Huet) critical pair theorem ⋮ Linguistic\(\leftrightarrow \)rational agents' semantics ⋮ Unifying sets and programs via dependent types ⋮ Differential (Lie) algebras from a functorial point of view ⋮ Deciding the word problem in the union of equational theories. ⋮ Decidability for left-linear growing term rewriting systems. ⋮ Categorification, term rewriting and the Knuth-Bendix procedure ⋮ On rewriting rules in Mizar ⋮ Transparent rule based CAS to support formalization of knowledge ⋮ Superposition decides the first-order logic fragment over ground theories ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ Unification modulo homomorphic encryption ⋮ A combined superposition and model evolution calculus ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Proof pearl: a formal proof of Higman's lemma in ACL2 ⋮ \(E\)-unification with constants vs. general \(E\)-unification ⋮ Best unifiers in transitive modal logics ⋮ Higher-dimensional normalisation strategies for acyclicity ⋮ Taylor term does not imply any nontrivial linear one-equality Maltsev condition ⋮ Linearity and iterator types for Gödel's system \(\mathcal T\) ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Theorem proving modulo ⋮ Confluence and convergence modulo equivalence in probabilistically terminating reduction systems ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Intensional computation with higher-order functions ⋮ Modeling dynamic programming problems over sequences and trees with inverse coupled rewrite systems ⋮ Relative locations of subwords in free operated semigroups and Motzkin words. ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Adding constants to string rewriting ⋮ A coherence theorem for pseudonatural transformations ⋮ Combalgebraic structures on decorated cliques ⋮ Satisfiability of general intruder constraints with and without a set constructor ⋮ On proving confluence modulo equivalence for Constraint Handling Rules ⋮ Abstract conjunctive partial deduction for the analysis and compilation of coroutines ⋮ Free operated monoids and rewriting systems ⋮ Colored operads, series on colored operads, and combinatorial generating systems ⋮ Normalization properties for shallow TRS and innermost rewriting ⋮ Verifying polymer reaction networks using bisimulation ⋮ Termination of narrowing via termination of rewriting ⋮ MetiTarski: An automatic theorem prover for real-valued special functions ⋮ A superposition calculus for abductive reasoning ⋮ On finite complete rewriting systems, finite derivation type, and automaticity for homogeneous monoids ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ On the complexity of deduction modulo leaf permutative equations ⋮ Reachability analysis over term rewriting systems ⋮ Constraint solving for proof planning ⋮ Termination of the F5 algorithm ⋮ Confluence and termination of fuzzy relations ⋮ A theory of reversibility for Erlang ⋮ Duality of graded graphs through operads ⋮ A logic based approach to finding real singularities of implicit ordinary differential equations ⋮ The Hydra battle and Cichon's principle ⋮ Undecidable properties of flat term rewrite systems ⋮ Constant runtime complexity of term rewriting is semi-decidable ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Equational theorem proving modulo ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ An automated approach to the Collatz conjecture ⋮ Derivational complexity and context-sensitive Rewriting ⋮ CHAP and rewrite components ⋮ Labelled splitting ⋮ Inductive proof search modulo ⋮ A local characterization of \(B_2\) regular crystals ⋮ Fast and parallel decomposition of constraint satisfaction problems ⋮ The lambda-context calculus (extended version) ⋮ Increasing interpretations ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols ⋮ Deciding the word problem for ground identities with commutative and extensional symbols ⋮ Relative undecidability in term rewriting. I: The termination hierarchy ⋮ Relative undecidability in term rewriting. II: The confluence hierarchy ⋮ Context-sensitive rewriting strategies ⋮ Equational rules for rewriting logic ⋮ ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT ⋮ From Logic to Functional Logic Programs ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ Sequoia: A Playground for Logicians ⋮ Controlled Term Rewriting ⋮ Congruence Closure of Compressed Terms in Polynomial Time ⋮ Generalized and Formalized Uncurrying ⋮ Type Inference for ZFH ⋮ Satisfiability Modulo Theories ⋮ Model Checking Security Protocols ⋮ Towards Erlang Verification by Term Rewriting ⋮ Modal Tableau Systems with Blocking and Congruence Closure ⋮ The combinator M and the Mockingbird lattice ⋮ Preserving consistency in geometric modeling with graph transformations ⋮ On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP ⋮ Certification of Termination Proofs Using CeTA ⋮ Transformations of Conditional Rewrite Systems Revisited ⋮ The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols ⋮ On some slowly terminating term rewriting systems ⋮ E-Unification based on Generalized Embedding ⋮ Algebraic data integration ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Semi-inversion of Conditional Constructor Term Rewriting Systems ⋮ Confluence up to Garbage ⋮ Unnamed Item ⋮ ALGORITHMIC PROBLEMS ON INVERSE MONOIDS OVER VIRTUALLY FREE GROUPS ⋮ EVANS' NORMAL FORM THEOREM REVISITED ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Theory of finite or infinite trees revisited ⋮ Unnamed Item ⋮ An insertion operator preserving infinite reduction sequences ⋮ Safety of Nöcker's strictness analysis ⋮ On rings of differential Rota–Baxter operators ⋮ Deciding Innermost Loops ⋮ Unnamed Item ⋮ Action of endomorphism semigroups on definable sets ⋮ Unnamed Item ⋮ Interacting quantum observables: categorical algebra and diagrammatics ⋮ Extensions of unification modulo ACUI ⋮ Bounded ACh unification ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Certifying a Termination Criterion Based on Graphs, without Graphs ⋮ Using groups for investigating rewrite systems ⋮ From Analytical Mechanics Problems to Rewriting Theory Through M. Janet’s Work ⋮ Noncommutative Gröbner Bases: Applications and Generalizations ⋮ Building language towers with Ziggurat ⋮ Congruence Closure with Free Variables ⋮ What Is Essential Unification? ⋮ Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting ⋮ Functional Logic Programming: From Theory to Curry ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Narrowing Based Inductive Proof Search ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ Multi-level modelling via stochastic multi-level multiset rewriting ⋮ Spans of cospans ⋮ ON CERTAIN PAIRS OF NON-ENGEL ELEMENTS IN FINITE GROUPS ⋮ Essentials of Term Graph Rewriting ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Universal enveloping algebras and Poincar\'e-Birkhoff-Witt theorem for involutive Hom-Lie algebras ⋮ From Outermost Termination to Innermost Termination ⋮ Superposition and Model Evolution Combined ⋮ Building Theorem Provers ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Beyond Dependency Graphs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms ⋮ On Transfinite Knuth-Bendix Orders ⋮ A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems ⋮ CSI – A Confluence Tool ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ First-class patterns ⋮ Welcome to Constraint Handling Rules ⋮ A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs ⋮ Monadic Datalog Tree Transducers ⋮ Termination of Priority Rewriting ⋮ Theories of orders on the set of words ⋮ Unnamed Item ⋮ Unnamed Item ⋮ REWRITING LOGIC-BASED SEMANTICS OF P SYSTEMS AND THE MAXIMAL CONCURRENCY ⋮ Loops under Strategies ⋮ Dependency Pairs and Polynomial Path Orders ⋮ Unique Normalization for Shallow TRS ⋮ Proving Confluence of Term Rewriting Systems Automatically ⋮ The $\Pi^0_2$ -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity) ⋮ Canonical Forms in Interactive Exercise Assistants ⋮ TAGED Approximations for Temporal Properties Model-Checking ⋮ Extending Maximal Completion (Invited Talk) ⋮ Unnamed Item ⋮ Term Sequent Logic ⋮ HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ ⋮ Expressivity and completeness for public update logics via reduction axioms ⋮ The adjoint semigroup of a $\Gamma$-semigroup ⋮ Unnamed Item ⋮ Automating Theories in Intuitionistic Logic ⋮ A CORRESPONDENCE BETWEEN BALANCED VARIETIES AND INVERSE MONOIDS ⋮ COMPOSITIONALITY, COMPUTABILITY, AND COMPLEXITY
Uses Software
