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 algorithmPRAMrepresentation of terms by directed acyclic graphsresolution theorem provingterm matching

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

(46)

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

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)