Sentence-normalized conditional narrowing modulo in rewriting logic and Maude

DOI10.1007/s10817-017-9417-5zbMath1398.68267OpenAlexW2295833488WikidataQ123905811 ScholiaQ123905811MaRDI QIDQ1655486

Isabel Pita, Miguel Palomino, Narciso Martí-Oliet, Luis Antonio Aguirre

Publication date: 9 August 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9417-5

zbMATH Keywords

reachabilityunificationnarrowingrewriting logicMaudemembership equational logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42)

Related Items

Using well-founded relations for proving operational termination

Uses Software

• Maude
• MTT
• Maude-NPA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rewriting logic and its applications. 10th international workshop, WRLA 2014, held as a satellite event of ETAPS, Grenoble, France, April 5--6, 2014. Revised selected papers
• Strict coherence of conditional rewriting modulo axioms
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• 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
• 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
• Completeness results for basic narrowing
• Maude: specification and programming in rewriting logic
• Rewriting logic: Roadmap and bibliography
• 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
• Proving operational termination of membership equational programs
• Semantic foundations for generalized rewrite theories
• Conditional Narrowing Modulo in Rewriting Logic and Maude
• Infinite-State Model Checking of LTLR Formulas Using Narrowing
• Rewriting Modulo SMT and Open System Analysis
• Model Checking LTLR Formulas under Localized Fairness
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• A needed narrowing strategy
• MTT: The Maude Termination Tool (System Description)
• Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
• Narrowing Based Inductive Proof Search
• Reachability in Conditional Term Rewriting Systems
• Operational Termination of Membership Equational Programs: the Order-Sorted Way