scientific article; zbMATH DE number 7455704

MaRDI QIDQ5020960zbMATH OpenFDO

Authors Damián Aparicio-Sánchez, Santiago Escobar, Julia Sapiña

Publication date 11 January 2022

Full work available at URL https://arxiv.org/abs/2009.11070, http://eptcs.web.cse.unsw.edu.au/paper.cgi?ICLP2020.10

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• Variant-based equational anti-unification
• Variant narrowing and equational unification
• Constructor equivalent term rewriting systems
• scientific article; zbMATH DE number 845921
• scientific article; zbMATH DE number 1678396
• Union of Reducibility Candidates for Orthogonal Constructor Rewriting
• Proving ground confluence and inductive validity in constructor based equational specifications
• scientific article; zbMATH DE number 125880
• Unifiers as equivalences: proof-relevant unification of dependently typed data
• scientific article; zbMATH DE number 1088023

Cites work

• Abstract logical model checking of infinite-state systems using narrowing
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Completion of a Set of Rules Modulo a Set of Equations
• Conditional rewriting logic as a unified model of concurrency
• Folding variant narrowing and optimal variant termination
• Generalized rewrite theories, coherence completion, and symbolic methods
• Ground confluence of order-sorted conditional specifications modulo axioms
• scientific article; zbMATH DE number 3817070 (Why is no real title available?)
• scientific article; zbMATH DE number 3821084 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 7453112 (Why is no real title available?)
• Matching, unification and complexity
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Modular Termination of Basic Narrowing
• Normal forms and normal theories in conditional rewriting
• On Forward Closure and the Finite Variant Property
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Programming and symbolic computation in Maude
• Rule-based unification in combined theories and the finite variant property
• Strict coherence of conditional rewriting modulo axioms
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Symbolic reasoning methods in rewriting logic and Maude
• Term Rewriting and Applications
• Termination Modulo Combinations of Equational Theories
• Termination of narrowing revisited
• Tests and proofs. 4th international conference, TAP 2010, Málaga, Spain, July 1--2, 2010. Proceedings
• Twenty years of rewriting logic
• Unification and matching in hierarchical combinations of syntactic theories
• Unification theory
• Using big-step and small-step semantics in Maude to perform declarative debugging
• Variant-Based Satisfiability in Initial Algebras

Cited in

(2)

• An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
• Variant-based equational anti-unification

Describes a project that uses

Uses Software

• Maude
• Maude-NPA

This page was built for publication:

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