Termination Modulo Combinations of Equational Theories
From MaRDI portal
Recommendations
- Modular termination of basic narrowing and equational unification
- scientific article; zbMATH DE number 2163052
- scientific article; zbMATH DE number 7204561
- On the modularity of termination of term rewriting systems
- Modular term rewriting systems and the termination
- Termination modulo equations by abstract commutation with an application to iteration
- Automated termination in model-checking modulo theories
- Automated Termination in Model Checking Modulo Theories
- scientific article; zbMATH DE number 992004
- Termination and completion modulo associativity, commutativity and identity
Cites work
- A total AC-compatible ordering based on RPO
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Combining matching algorithms: The regular case
- Complete Sets of Reductions for Some Equational Theories
- Completion for rewriting modulo a congruence
- Completion of a Set of Rules Modulo a Set of Equations
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Effectively Checking the Finite Variant Property
- Equational rules for rewriting logic
- scientific article; zbMATH DE number 1670496 (Why is no real title available?)
- scientific article; zbMATH DE number 1722701 (Why is no real title available?)
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 4060701 (Why is no real title available?)
- scientific article; zbMATH DE number 1552528 (Why is no real title available?)
- scientific article; zbMATH DE number 1414317 (Why is no real title available?)
- MTT: The Maude Termination Tool (System Description)
- Operational termination of membership equational programs: the order-sorted way
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Proving operational termination of membership equational programs
- Term Rewriting and Applications
- Termination and completion modulo associativity, commutativity and identity
- Termination Modulo Combinations of Equational Theories
- Termination of rewriting systems by polynomial interpretations and its implementation
- Variant narrowing and equational unification
Cited in
(32)- Termination and completion modulo associativity, commutativity and identity
- Termination modulo equations by abstract commutation with an application to iteration
- Twenty years of rewriting logic
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Symbolic computation in Maude: some tapas
- Order-sorted equational generalization algorithm revisited
- Proving operational termination of membership equational programs
- Ground confluence of order-sorted conditional specifications modulo axioms
- Metalevel algorithms for variant satisfiability
- Modular and incremental proofs of AC-termination
- Built-in variant generation and unification, and their applications in Maude 2.7
- Algebraic Notions of Termination
- scientific article; zbMATH DE number 3870640 (Why is no real title available?)
- Termination Modulo Combinations of Equational Theories
- scientific article; zbMATH DE number 4047065 (Why is no real title available?)
- scientific article; zbMATH DE number 2043543 (Why is no real title available?)
- scientific article; zbMATH DE number 7453112 (Why is no real title available?)
- scientific article; zbMATH DE number 7455704 (Why is no real title available?)
- Dummy elimination in equational rewriting
- scientific article; zbMATH DE number 7566074 (Why is no real title available?)
- scientific article; zbMATH DE number 7204561 (Why is no real title available?)
- Operational termination of membership equational programs: the order-sorted way
- AC dependency pairs revisited
- An universal termination condition for solving goals in equational languages
- Variants and satisfiability in the infinitary unification wonderland
- Checking Sufficient Completeness by Inductive Theorem Proving
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- Building correct-by-construction systems with formal patterns
- Strict coherence of conditional rewriting modulo axioms
- Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
- Normal forms and normal theories in conditional rewriting
- Enabledness and termination in refinement algebra
This page was built for publication: Termination Modulo Combinations of Equational Theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3655204)
