Variants and satisfiability in the infinitary unification wonderland

DOI10.1016/j.jlamp.2023.100877OpenAlexW4378982347MaRDI QIDQ6113018

No author found.

Publication date: 8 August 2023

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2023.100877

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An efficient SMT solver for string constraints
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Complete axiomatizations of some quotient term algebras
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Complexity, convexity and combinations of theories
• Conditional rewriting logic as a unified model of concurrency
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Combining unification algorithms
• Variant-based decidable satisfiability in initial algebras with predicates
• Structured theories and institutions
• Unification in the union of disjoint equational theories: Combining decision procedures
• Modularity in term rewriting revisited
• Folding variant narrowing and optimal variant termination
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
• 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
• Metalevel algorithms for variant satisfiability
• Language Prototyping: An Algebraic Specification Approach
• On Forward Closure and the Finite Variant Property
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• An Evaluation of Automata Algorithms for String Analysis
• Order-Sorted Parameterization and Induction
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Termination Modulo Combinations of Equational Theories
• Coding in the existential theory of concatenation
• Simplification by Cooperating Decision Procedures
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Variant-Based Satisfiability in Initial Algebras
• A Constructor-Based Reachability Logic for Rewrite Theories
• Order-sorted Equational Unification Revisited
• Logics in Artificial Intelligence
• Term Rewriting and Applications

This page was built for publication: Variants and satisfiability in the infinitary unification wonderland