On the sequential nature of unification

DOI10.1016/0743-1066(84)90022-0zbMath0588.68045OpenAlexW1982801224MaRDI QIDQ3716320

John C. Mitchell, Cynthia Dwork, Paris C. Kanellakis

Publication date: 1984

Published in: The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0743-1066(84)90022-0

zbMATH Keywords

parallel algorithmPRAMresolution theorem provingterm matchingrepresentation of terms by directed acyclic graphs

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Graph theory (including graph drawing) in computer science (68R10)

Related Items (28)

Exploiting parallelism in coalgebraic logic programming ⋮ A parallel algorithm for the monadic unification problem ⋮ A theory of strict P-completeness ⋮ Fine-grained concurrent completion ⋮ Unique normal forms for nonlinear term rewriting systems: Root overlaps ⋮ Associative-commutative unification ⋮ An efficient labelled nested multiset unification algorithm ⋮ A practically efficient and almost linear unification algorithm ⋮ On the relationship of congruence closure and unification ⋮ Classifying the computational complexity of problems ⋮ Automatic theorem proving. II ⋮ Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ An analysis of the Core-ML language: Expressive power and type reconstruction ⋮ Optimal parallel algorithms for forest and term matching ⋮ Average-case analysis of unification algorithms ⋮ Another variation on the common subexpression problem ⋮ A note on the parallel complexity of anti-unification ⋮ Efficient parallel term matching and anti-unification ⋮ Tight complexity bounds for term matching problems ⋮ C-expressions: A variable-free calculus for equational logic programming ⋮ Type inference with simple subtypes ⋮ Unnamed Item ⋮ Unary Resolution: Characterizing Ptime ⋮ Some complexity bounds for subtype inequalities ⋮ A theory of strict P-completeness ⋮ On the logic of unification ⋮ The complexity of the satisfiability problem for Krom formulas ⋮ The complexity of type inference for higher-order typed lambda calculi

This page was built for publication: On the sequential nature of unification