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

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