Folding variant narrowing and optimal variant termination
From MaRDI portal
Publication:1931909
DOI10.1016/j.jlap.2012.01.002zbMath1291.68217OpenAlexW2316113835MaRDI QIDQ1931909
José Meseguer, Ralf Sasse, Santiago Escobar
Publication date: 16 January 2013
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2012.01.002
Related Items (38)
Non-disjoint combined unification and closure by equational paramodulation ⋮ Order-sorted equational generalization algorithm revisited ⋮ Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Metalevel algorithms for variant satisfiability ⋮ José Meseguer: Scientist and Friend Extraordinaire ⋮ Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude ⋮ Alice and Bob Meet Equational Theories ⋮ Two Decades of Maude ⋮ Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Symbolic Analysis of Maude Theories with Narval ⋮ Variant-based equational anti-unification ⋮ Strategies in conditional narrowing modulo SMT plus axioms ⋮ Optimizing Maude programs via program specialization ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols ⋮ Functional Logic Programming in Maude ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ 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 ⋮ Automated Verification of Equivalence Properties of Cryptographic Protocols ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ Equational theorem proving modulo ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms* ⋮ Capturing constrained constructor patterns in matching logic ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas ⋮ Terminating non-disjoint combined unification
Uses Software
This page was built for publication: Folding variant narrowing and optimal variant termination
