Strict coherence of conditional rewriting modulo axioms
From MaRDI portal
Publication:683741
DOI10.1016/j.tcs.2016.12.026zbMath1386.68080OpenAlexW2282814833MaRDI QIDQ683741
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
coherenceoperational terminationChurch-Rosser propertyconditional rewriting modulo equationsorder-sorted specifications
Related Items
Sentence-normalized conditional narrowing modulo in rewriting logic and Maude, Optimization of rewrite theories by equational partial evaluation, Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude, An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis, Variant-based equational anti-unification, Strategies in conditional narrowing modulo SMT plus axioms, Unnamed Item, Unnamed Item, Variant-Based Satisfiability in Initial Algebras, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, A partial evaluation framework for order-sorted equational programs modulo axioms, Ground confluence of order-sorted conditional specifications modulo axioms, Metalevel Algorithms for Variant Satisfiability, Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), Symbolic computation in Maude: some tapas
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Order-sorted unification
- Normal forms and normal theories in conditional rewriting
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Operational termination of conditional term rewriting systems
- A mechanical solution of Schubert's steamroller by many-sorted resolution
- Conditional rewrite rules
- A more expressive formulation of many sorted logic
- Conditional rewrite rules: Confluence and termination
- Inheritance hierarchies: Semantics and unifications
- A Noetherian and confluent rewrite system for idempotent semigroups
- The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
- Conditional rewriting logic as a unified model of concurrency
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Conditional narrowing modulo a set of equations
- Completion for rewriting modulo a congruence
- 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
- CASL user manual. Introduction to using the Common Algebraic Specification Language. With chapters by Till Mossakowski, Donald Sannella, and Andrzej Tarlecki. With CD-ROM.
- A resolution principle for a logic with restricted quantifiers
- ELAN from a rewriting logic point of view
- Equational rules for rewriting logic
- Computational aspects of an order-sorted logic with term declarations
- A structural approach to operational semantics
- CASL reference manual. The complete documentation of the common algebraic specification language.
- Twenty years of rewriting logic
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Folding variant narrowing and optimal variant termination
- Specification and proof in membership equational logic
- Logicality of conditional rewrite systems
- Proving operational termination of membership equational programs
- Semantic foundations for generalized rewrite theories
- Language Prototyping: An Algebraic Specification Approach
- Methods for Proving Termination of Rewriting-based Programming Languages by Transformation
- Rewriting Modulo SMT and Open System Analysis
- Termination Modulo Combinations of Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Complete Sets of Reductions for Some Equational Theories
- Inclusions and subtypes II: higher-order case
- Order-sorted Equational Unification Revisited
- Equality, types, modules, and (why not?) generics for logic programming
