Sentence-normalized conditional narrowing modulo in rewriting logic and Maude

DOI10.1007/S10817-017-9417-5MaRDI QIDQ1655486zbMATH OpenOpenAlexWikidataFDO

Authors Narciso Martí-Oliet, Miguel Palomino, Isabel Pita, 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

reachabilityunificationrewriting logicMaudenarrowingmembership equational logic

Mathematics Subject Classification ID

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

Recommendations

• Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
• Conditional narrowing modulo in rewriting logic and Maude
• Reachability in conditional term rewriting systems
• Narrowing and rewriting logic: from foundations to applications
• A constructor-based reachability logic for rewrite theories

Cites work

• scientific article; zbMATH DE number 4053008 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3467029 (Why is no real title available?)
• scientific article; zbMATH DE number 1497855 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A needed narrowing strategy
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Completeness results for basic narrowing
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Completion of rewrite systems with membership constraints. II: Constraint solving
• Conditional narrowing modulo a set of equations
• Conditional narrowing modulo in rewriting logic and Maude
• Folding variant narrowing and optimal variant termination
• Infinite-state model checking of LTLR formulas using narrowing
• MTT: The Maude Termination Tool (System Description)
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Maude: specification and programming in rewriting logic
• Model checking LTLR formulas under localized fairness
• Narrowing based inductive proof search
• Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Operational termination of conditional term rewriting systems
• Operational termination of membership equational programs: the order-sorted way
• Proving operational termination of membership equational programs
• Reachability in conditional term rewriting systems
• 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
• Rewriting logic: Roadmap and bibliography
• Rewriting modulo SMT and open system analysis
• Semantic foundations for generalized rewrite theories
• Strict coherence of conditional rewriting modulo axioms
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Twenty years of rewriting logic

Cited in

(4)

• Using well-founded relations for proving operational termination
• Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
• Strategies in conditional narrowing modulo SMT plus axioms
• Conditional narrowing modulo in rewriting logic and Maude

Describes a project that uses

Uses Software

• Maude-NPA
• MTT
• Maude

This page was built for publication: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1655486)