Efficient parallel term matching and anti-unification

Arthur L. Delcher, Simon Kasif

Research output: Contribution to journalArticlepeer-review


In this paper we present optimal processor x time parallel algorithms for term matching and anti-unification of terms represented as trees. Term matching is the special case of unification in which one of the terms is restricted to contain no variables. It has wide applicability to logic programming, term rewriting systems and symbolic pattern matching. Anti-unification is the dual problem of unification in which one computes the most specific generalization of two terms. It has application to inductive inference and theorem proving. Our algorithms run in O(log2N) time using N/log2N processors on a shared-memory model of computation that prohibits simultaneous reads or writes (EREW PRAM). These algorithms are the first polylogarithmic-time EREW algorithms with a processor x time product of the same order as that of their sequential counterparts, thereby permitting optimal speed-ups using any number of processors up to N/log2N. We also use the techniques developed in the paper to provide an N/log N-processor, O(log N)-time algorithm for a shared-memory model that allows both simultaneous reads and simultaneous writes (CRCW PRAM).

Original languageEnglish (US)
Pages (from-to)391-406
Number of pages16
JournalJournal of Automated Reasoning
Issue number3
StatePublished - Dec 1 1992


  • Parallel algorithms
  • anti-unification
  • term matching

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


Dive into the research topics of 'Efficient parallel term matching and anti-unification'. Together they form a unique fingerprint.

Cite this