Solvability of context equations with two context variables is decidable

DOI10.1006/JSCO.2001.0438MaRDI QIDQ1599536zbMATH OpenOpenAlexFDO

Authors K. U. Schulz, Manfred Schmidt-Schauß

Publication date 11 June 2002

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1006/jsco.2001.0438

zbMATH Keywords

context unification

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1341608
• How to prove decidability of equational theories with second-order computation analyser SOL
• Decidability of affine solution problems
• Two Definability Results in the Equational Context
• scientific article; zbMATH DE number 1186371
• SOLVABILITY OF EQUATIONS IN GRAPH GROUPS IS DECIDABLE
• Some decidable results on reachability of solvable systems
• scientific article; zbMATH DE number 3174467
• The satisfiability of word equations: decidable and undecidable theories
• On Solvable Congruences in Finitely Decidable Varieties

Cites work

• scientific article; zbMATH DE number 1189059 (Why is no real title available?)
• scientific article; zbMATH DE number 1222595 (Why is no real title available?)
• scientific article; zbMATH DE number 1341608 (Why is no real title available?)
• A decision algorithm for distributive unification
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Completion of rewrite systems with membership constraints. II: Constraint solving
• Complexity of Makanin's algorithm
• Equations in free semigroups
• Linear second-order unification
• Minimal and complete word unification
• On the undecidability of second-order unification
• Solving word equations
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• The undecidability of the second-order unification problem
• Undecidability of the first order theory of one-step right ground rewriting
• Unification in the union of disjoint equational theories: Combining decision procedures
• Word unification and transformation of generalized equations

Cited in

(11)

• Automated Deduction – CADE-20
• Flat matching
• Simplifying the signature in second-order unification
• Dominance constraints in stratified context unification
• Deciding context unification
• scientific article; zbMATH DE number 1722705 (Why is no real title available?)
• On rewrite constraints and context unification
• Decidability of bounded second order unification
• Decidability of bounded higher-order unification
• Context unification with one context variable
• Deciding context unification (with regular constraints)

This page was built for publication: Solvability of context equations with two context variables is decidable

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