Two-restricted one context unification is in polynomial time

DOI10.4230/LIPICS.CSL.2015.405MaRDI QIDQ5351971zbMATH OpenOpenAlexFDO

Authors Adrià Gascón, Manfred Schmidt-Schauß, Ashish Tiwari

Publication date 31 August 2017

Full work available at URL https://dblp.uni-trier.de/db/conf/csl/csl2015.html#GasconST15

zbMATH Keywords

context unificationdeductionfirst-order unificationtype checking

Mathematics Subject Classification ID

Logic in computer science (03B70) Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Recommendations

• One context unification problems solvable in polynomial time
• Context unification with one context variable
• Deciding context unification
• One-context unification with STG-compressed terms is in NP
• Automated Deduction – CADE-20

Cited in

(5)

• Context unification with one context variable
• Stratified Context Unification Is NP-Complete
• One context unification problems solvable in polynomial time
• One-context unification with STG-compressed terms is in NP
• Automated Deduction – CADE-20

This page was built for publication: Two-restricted one context unification is in polynomial time

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