Unification modulo lists with reverse relation with certain word equations

DOI10.1007/978-3-030-29436-6_1MaRDI QIDQ2305403zbMATH OpenOpenAlexFDO

Authors Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch

Publication date 10 March 2020

Full work available at URL https://doi.org/10.1007/978-3-030-29436-6_1

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Unification Modulo Chaining
• Solving word equations modulo partial commutations
• Unification and matching modulo nilpotence
• Unification and Matching Modulo Leaf-Permutative Equational Presentations
• Word unification and transformation of generalized equations
• scientific article; zbMATH DE number 1346492
• Solving equations on words with morphisms and antimorphisms
• Unification modulo \(\alpha\)-equivalence in a mathematical assistant system
• Recursively Enumerable Equivalence Relations Modulo Finite Differences
• scientific article; zbMATH DE number 1189063

Cites work

• A decision procedure for regular membership and length constraints over unbounded strings
• Abstract Data Type Specification in the Affirm System
• Abstract data types and software validation
• An efficient algorithm for solving word equations
• Deciding Combinations of Theories
• Finding all solutions of equations in free groups and monoids with involution
• scientific article; zbMATH DE number 1304322 (Why is no real title available?)
• scientific article; zbMATH DE number 2079035 (Why is no real title available?)
• scientific article; zbMATH DE number 2149521 (Why is no real title available?)
• New results on rewrite-based satisfiability procedures
• On word equations in one variable
• Proof by consistency
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• Reasoning About Recursively Defined Data Structures
• Simplification by Cooperating Decision Procedures
• Term Rewriting and All That
• Unification in the union of disjoint equational theories: Combining decision procedures
• Unification modulo lists with reverse relation with certain word equations
• Unification theory
• Universality of a reversible two-counter machine

Cited in

(1)

• Unification modulo lists with reverse relation with certain word equations

This page was built for publication: Unification modulo lists with reverse relation with certain word equations

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