Article

Free access

Parallel algorithms for unification and other complete problems in p

Authors:

Jeffrey Scott Vitter,

Roger A. SimonsAuthors Info & Claims

ACM '84: Proceedings of the 1984 annual conference of the ACM on The fifth generation challenge

Pages 75 - 84

https://doi.org/10.1145/800171.809607

Published: 01 January 1984 Publication History

Abstract

Unification is a basic operation in theorem proving, in type inference algorithms, and in logic programming languages such as Prolog. Prolog will play a major role in software development for the Fifth Generation project, and thus developing fast algorithms for unification is an important goal. This paper shows that the running time for a linear unification algorithm can often be improved substantially by use of parallel processing. The same is true for algorithms for some other complete problems in P, namely, the monotone circuit value problem and the path system accessibility problem. Previous theoretical work in computational complexity has suggested that these problems are not parallelizable; in practice this is not the case. To resolve this paradox, we introduce new complexity classes PC and PC* that capture the practical notion of parallelizability we discuss in this paper. We pose several open questions concerning PC and PC*.

References

[1]

A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, MA (1974).

Digital Library

[2]

A. K. Chandra, L. Stockmeyer, and U. Vishkin. Constant Depth Reducibility. SIAM Journal on Computing 13, 2 (May 1984), 423-439.

[3]

W. F. Clocksin and C. S. Mellish. Programming in Prolog. Springer-Verlag, New York (1981).

Digital Library

[4]

S. A. Cook. An Observation on Time-Storage Trade Off. Journal of Computer and System Sciences 9 (1974), 308-316.

[5]

S. A. Cook. An Overview of Computational Complexity. Communications of the ACM 26, 6 (June 1983), 400-408.

Digital Library

[6]

C. Dwork, P. C. Kanellakis, and J. C. Mitchell. On the Sequential Nature of Unification. Journal of Logic Programming 1, 1 (June 1984).

Digital Library

[7]

S. Fortune and J. Wyllie. Parallelism in Random Access Machines. Proceedings of the 10th Annual ACM Symposium on Theory of Computing, San Diego, CA (May 1978), 114-118.

Digital Library

[8]

M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco (1979).

Digital Library

[9]

L. M. Goldschlager. The Monotone and Planar Circuit Value Problems are Log Space Complete for P. SIGACT News 9, 2 (1977), 25-29.

Digital Library

[10]

D. S. Johnson. The NP-Completeness Column: An On-going Guide. Journal of Algorithms 4, 2 (June 1983), 189-203.

[11]

P. C. Kanellakis. Personal Communication (February 1984).

[12]

D. MacQueen, G. Plotkin, and R. Sethi. An Ideal Model for Recursive Polymorphic Types. Proceedings of the 11th Annual ACM Symposium on Principles of Programming Languages, Salt Lake City, UT (January 1984).

Digital Library

[13]

A. Martelli and U. Montanari. Unification in Linear Time and Space: A Structured Presentation. Internal Report B76-16, Consiglio Nazionale delle Ricerche, Pisa, Italy (July 1976).

[14]

R. Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, 3 (December 1978), 348-375.

[15]

M. S. Paterson and M. N. Wegman. Linear Unification. Journal of Computer and System Sciences 16, 2 (April 1978), 158-167.

[16]

N. Pippenger. On Simultaneous Resource Bounds. Proceedings of the 20th Annual IEEE Symposium on Foundations of Computer Science, San Juan, Puerto Rico (October 1979), 307-311.

Digital Library

[17]

J. A. Robinson. Computational Logic: the Unification Computation. Machine Intelligence 6, (1971), 63-72.

[18]

J. E. Savage and J. S. Vitter. Parallelism in Space-Time Tradeoffs. Proceedings of the International Workshop on VLSI: Algorithms and Architectures, Amalfi, Italy (May 1984). Published by North-Holland.

[19]

E. Y. Shapiro. A Subset of Concurrent Prolog and its Interpreter. Technical Report TR-003, Institute for New Generation Computer Technology, Tokyo (1983).

[20]

Y. Shiloach and U. Vishkin. Finding the Maximum, Merging, and Sorting in a Parallel Computation Model. Journal of Algorithms 2 (1981), 88-102.

[21]

L. Stockmeyer and U. Vishkin. Simulation of Parallel Random Access Machines by Circuits. SIAM Journal on Computing 13, 2 (May 1984), 409-422.

[22]

R. E. Tarjan. Data Structures and Network Algorithms. SIAM, Philadelphia (1983).

Digital Library

[23]

J. S. Vitter and R. A. Simons. New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems in P. Technical Report CS-84-06, Brown University (June 1984).

[24]

H. Yasuura. On the Parallel Computational Complexity of Unification. Research Report ER 83-01, Yajima Lab., Kyoto University October 12, 1983).

Cited By

Weber V(1993)Connectionist Unifying PrologArtificial Neural Nets and Genetic Algorithms10.1007/978-3-7091-7533-0_32(213-220)Online publication date: 1993
https://doi.org/10.1007/978-3-7091-7533-0_32
Ponder C(1988)Parallelism and algorithms for algebraic manipulation: current workACM SIGSAM Bulletin10.1145/49456.4945722:3(7-14)Online publication date: 1-Jul-1988
https://dl.acm.org/doi/10.1145/49456.49457
Varman PDoshi KDavis PMcClintock V(1987)Improved parallel algorithms for the depth-first search and monotone circuit value problemsProceedings of the 15th annual conference on Computer Science10.1145/322917.322945(175-182)Online publication date: 1-Feb-1987
https://dl.acm.org/doi/10.1145/322917.322945
Show More Cited By

Index Terms

Parallel algorithms for unification and other complete problems in p
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Computational complexity and cryptography
    1. Complexity classes

Recommendations

Undecidability of the unification and admissibility problems for modal and description logics

We show that the unification problem “is there a substitution instance of a given formula that is provable in a given logic?” is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem ...
Complete sets of transformations for general unification
Unification nets: canonical proof net quantifiers
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard's ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ACM '84: Proceedings of the 1984 annual conference of the ACM on The fifth generation challenge

January 1984

336 pages

ISBN:089791144X

DOI:10.1145/800171

Copyright © 1984 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1984

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
348
Total Downloads

Downloads (Last 12 months)30
Downloads (Last 6 weeks)6

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Weber V(1993)Connectionist Unifying PrologArtificial Neural Nets and Genetic Algorithms10.1007/978-3-7091-7533-0_32(213-220)Online publication date: 1993
https://doi.org/10.1007/978-3-7091-7533-0_32
Ponder C(1988)Parallelism and algorithms for algebraic manipulation: current workACM SIGSAM Bulletin10.1145/49456.4945722:3(7-14)Online publication date: 1-Jul-1988
https://dl.acm.org/doi/10.1145/49456.49457
Varman PDoshi KDavis PMcClintock V(1987)Improved parallel algorithms for the depth-first search and monotone circuit value problemsProceedings of the 15th annual conference on Computer Science10.1145/322917.322945(175-182)Online publication date: 1-Feb-1987
https://dl.acm.org/doi/10.1145/322917.322945
Wah BLi G(1986)Survey on special purpose computer architectures for AIACM SIGART Bulletin10.1145/15715.15718(28-46)Online publication date: 1-Apr-1986
https://dl.acm.org/doi/10.1145/15715.15718
Vitter JSimons R(1986)New Classes for Parallel ComplexityIEEE Transactions on Computers10.1109/TC.1986.167678335:5(403-418)Online publication date: 1-May-1986
https://dl.acm.org/doi/10.1109/TC.1986.1676783
Balbin ILecot KBalbin ILecot K(1985)Theoretical Issues of Logic ProgrammingLogic Programming10.1007/978-94-009-5044-3_2(10-60)Online publication date: 1985
https://doi.org/10.1007/978-94-009-5044-3_2

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents