On the sequential nature of unification

DOI10.1016/0743-1066(84)90022-0MaRDI QIDQ3716320zbMATH OpenOpenAlexFDO

Authors Cynthia Dwork, Paris C. Kanellakis, John Mitchell

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)

Recommendations

• scientific article; zbMATH DE number 4049127
• Efficient parallel term matching and anti-unification
• Tight complexity bounds for term matching problems
• Some results on equational unification
• scientific article; zbMATH DE number 3995082

Cited in

(43)

• Unique normal forms for nonlinear term rewriting systems: Root overlaps
• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
• C-expressions: A variable-free calculus for equational logic programming
• scientific article; zbMATH DE number 2064226 (Why is no real title available?)
• 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
• The complexity of the satisfiability problem for Krom formulas
• scientific article; zbMATH DE number 4047099 (Why is no real title available?)
• Efficient tree pattern unification
• On determining the causes of nonunifiability
• On the relationship of congruence closure and unification
• Unifications, deunifications, and their complexity
• Optimal parallel algorithms for forest and term matching
• The complexity of type inference for higher-order typed lambda calculi
• An analysis of the Core-ML language: Expressive power and type reconstruction
• Type inference with simple subtypes
• Associative-commutative unification
• scientific article; zbMATH DE number 522867 (Why is no real title available?)
• scientific article; zbMATH DE number 4049127 (Why is no real title available?)
• An efficient labelled nested multiset unification algorithm
• Exploiting parallelism in coalgebraic logic programming
• scientific article; zbMATH DE number 1615233 (Why is no real title available?)
• scientific article; zbMATH DE number 3858458 (Why is no real title available?)
• A practically efficient and almost linear unification algorithm
• A theory of strict P-completeness
• A theory of strict P-completeness
• Fine-grained concurrent completion
• Automata-driven efficient subterm unification
• Classifying the computational complexity of problems
• Term matching on parallel computers
• Tight complexity bounds for term matching problems
• Rational unification in 28 characters
• On the logic of unification
• New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems for P
• scientific article; zbMATH DE number 1389857 (Why is no real title available?)
• Some complexity bounds for subtype inequalities
• A parallel algorithm for the monadic unification problem
• Automatic theorem proving. II
• scientific article; zbMATH DE number 6917940 (Why is no real title available?)
• Unary resolution: characterizing \textsc{Ptime}
• Set-term unification in a logic database language

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

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