Matching, unification and complexity

Publisher Website
Google Scholar
Abstract
Pattern matching and unification are two key primitive operations used in many inference based systems including theorem provers, term rewriting systems, computer algebra systems, deductive data bases, Prolog, logic programming systems, functional language systems, systems for analysis of specifications and program synthesis, and program verification systems. In this note, we give results recently obtained in studying the complexity of matching and unification problems for first-order terms especially when some function symbols are interpreted. For further details and proofs, the reader may wish to refer to a forthcoming paper by the authors.

This publication has 2 references indexed in Scilit: