Strict coherence of conditional rewriting modulo axioms
From MaRDI portal
Publication:683741
DOI10.1016/J.TCS.2016.12.026zbMATH Open1386.68080OpenAlexW2282814833MaRDI QIDQ683741FDOQ683741
Authors: José Meseguer 
Publication date: 9 February 2018
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2016.12.026
Recommendations
coherenceoperational terminationChurch-Rosser propertyconditional rewriting modulo equationsorder-sorted specifications
Cites Work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- A mechanical solution of Schubert's steamroller by many-sorted resolution
- A structural approach to operational semantics
- Title not available (Why is that?)
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Title not available (Why is that?)
- Rewriting
- Complete Sets of Reductions for Some Equational Theories
- A resolution principle for a logic with restricted quantifiers
- Title not available (Why is that?)
- CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
- Title not available (Why is that?)
- Title not available (Why is that?)
- CASL reference manual. The complete documentation of the common algebraic specification language.
- Operational termination of conditional term rewriting systems
- Conditional rewrite rules
- Conditional rewrite rules: Confluence and termination
- Conditional rewriting logic as a unified model of concurrency
- Equational rules for rewriting logic
- Twenty years of rewriting logic
- Proving operational termination of membership equational programs
- Semantic foundations for generalized rewrite theories
- Rewriting modulo SMT and open system analysis
- Title not available (Why is that?)
- Normal forms and normal theories in conditional rewriting
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Language prototyping: An algebraic specification approach
- Specification and proof in membership equational logic
- Title not available (Why is that?)
- CASL user manual. Introduction to using the Common Algebraic Specification Language. With chapters by Till Mossakowski, Donald Sannella, and Andrzej Tarlecki. With CD-ROM.
- Completion of a Set of Rules Modulo a Set of Equations
- Inheritance hierarchies: Semantics and unifications
- A Noetherian and confluent rewrite system for idempotent semigroups
- Computational aspects of an order-sorted logic with term declarations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Order-sorted equational unification revisited
- Order-sorted unification
- Equality, types, modules, and (why not?) generics for logic programming
- ELAN from a rewriting logic point of view
- Completion for rewriting modulo a congruence
- A more expressive formulation of many sorted logic
- The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
- Conditional narrowing modulo a set of equations
- Completion of rewrite systems with membership constraints. I: Deduction rules
- Completion of rewrite systems with membership constraints. II: Constraint solving
- Order-sorted algebraic specifications with higher-order functions
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Folding variant narrowing and optimal variant termination
- Logicality of conditional rewrite systems
- Title not available (Why is that?)
- Methods for proving termination of rewriting-based programming languages by transformation
- Termination Modulo Combinations of Equational Theories
- Title not available (Why is that?)
- Inclusions and subtypes II: higher-order case
Cited In (21)
- Order-sorted homeomorphic embedding modulo combinations of associativity and/or commutativity axioms
- Generalized rewrite theories, coherence completion, and symbolic methods
- Symbolic computation in Maude: some tapas
- A partial evaluation framework for order-sorted equational programs modulo axioms
- Ground confluence of order-sorted conditional specifications modulo axioms
- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
- Strategies in conditional narrowing modulo SMT plus axioms
- Generalized rewrite theories and coherence completion
- Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
- Title not available (Why is that?)
- Title not available (Why is that?)
- An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
- Programming and symbolic computation in Maude
- Tactics for Reasoning Modulo AC in Coq
- Optimization of rewrite theories by equational partial evaluation
- Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method
- Variant-based equational anti-unification
- Variant-Based Satisfiability in Initial Algebras
- Metalevel algorithms for variant satisfiability
- A Maude coherence checker tool for conditional order-sorted rewrite theories
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Uses Software
This page was built for publication: Strict coherence of conditional rewriting modulo axioms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q683741)
