On equality up-to constraints over finite trees, context unification, and one-step rewriting

DOI10.1007/3-540-63104-6_4zbMath1430.68137OpenAlexW1854915563MaRDI QIDQ5234685

Joachim Niehren, Manfred Pinkal, Peter Ruhrberg

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00536822/file/fullContext.pdf

zbMATH Keywords

string unificationcontext unificationtree constraintsone-step rewritingsubtree relationsemantic processing of natural languagelinear second-order unification

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42) Natural language processing (68T50) Computational aspects of satisfiability (68R07)

Related Items

Decidability of bounded higher-order unification, Grid structures and undecidable constraint theories, A decision algorithm for distributive unification, The first-order theory of linear one-step rewriting is undecidable, On equality up-to constraints over finite trees, context unification, and one-step rewriting, Context unification with one context variable, On the undecidability of second-order unification, On rewrite constraints and context unification, \(\forall \exists^{5}\)-equational theory of context unification is undecidable

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solutions principales et rang d'un système d'équations avec constantes dans le monoide libre
• The undecidability of the second-order unification problem
• A new method for undecidability proofs of first order theories
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Completion of rewrite systems with membership constraints. II: Constraint solving
• Decidability of the existential theory of infinite terms with subterm relation
• Word unification and transformation of generalized equations
• Minimal and complete word unification
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Complexity of Makanin's algorithm
• Undecidability of the first order theory of one-step right ground rewriting
• The first-order theory of one step rewriting in linear noetherian systems is undecidable
• Encompassment properties and automata with constraints
• The first-order theory of one-step rewriting is undecidable
• Linear second-order unification
• On equality up-to constraints over finite trees, context unification, and one-step rewriting
• A Complete Mechanization of Second-Order Type Theory