Parallel theorem proving with connection graphs | SpringerLink
Skip to main content
Springer Nature Link
Log in

Parallel theorem proving with connection graphs

  • Graph Based Deduction
  • Conference paper
  • First Online:
8th International Conference on Automated Deduction (CADE 1986)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 230))

Included in the following conference series:

Abstract

In general, theorem provers are relatively slow. Speed up can be achieved by directing the search towards finding a proof and by using parallelism. The parallelisms identified in connection graph refutations are: or parallelism, and parallelism, and dcdp parallelism.

In dcdp parallelism, the links (edges) incident to distinct clauses and edge disjoint pairs are resolved in parallel. Optimally selecting potential parallel links is equivalent to solving the optimal graph coloring problem. Fortunately, however, optimal solutions to this NP-hard problem are not crucial. We describe a parallel solution of a sub-optimal graph coloring algorithm

In and parallelism, all literals in the sun clause are resolved concurrently and all the resolvents obtained. The resolvents, along with their inherited links, are inserted into the graph. The sun clause, and all the links connected to it, are removed from the graph. Because shared variables are restricted to have the same instantiation when there are shared variables in the sun clause, resolving literals concurrently becomes difficult. We discuss different approaches for performing this and parallelism.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. M. Bruynooghe. The inheritance of links in connection graph and its relation to structure sharing. Technical Report, Applied Mathematics and Programming Division, Katholieke Universiteit, Katholieke universiteit, Leuven, Belgium., 1977.

    Google Scholar 

  2. G. J. Chaitin, M. A. Auslander, A. K. Chandra, J. Cocke, M. E. Hopkins, and P. W. Markstein. Register allocation via coloring. Computer Languages, 6:47–57, 1981.

    Article  Google Scholar 

  3. C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17:698–707, October 1970.

    Article  Google Scholar 

  4. C. L. Chang and R. C. T. Lee. Symbolic Logic and Mechnical Theorem Proving. Academic Press, New York, 1973.

    Google Scholar 

  5. J. S. Conery. The AND/OR process model for parallel interpretation of logic programs. PhD thesis, University of California, Irvine, June 1983.

    Google Scholar 

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

    Google Scholar 

  7. G. Hornung, A. Knapp, and U. Knapp. A parallel connection graph proof procedure. In German Workshop on Artificial Intelligence. Lecture Notes in Computer Science, pages 160–167, Berlin: Springer-Verlag, 1981.

    Google Scholar 

  8. R. Kowalski. Logic for Problem Solving. Elsevier-North Holland, New York, 1979.

    Google Scholar 

  9. R. Kowalski. A proof procedure using connection graphs. Journal of the ACM, 22(4):572–595, October 1975.

    Article  Google Scholar 

  10. R. Kowalski and D. Kuchner. Linear resolution with selection function. In Artificial Intelligence, pages 221–260, 1971.

    Google Scholar 

  11. R. Loganantharaj. Theoretical and implementational aspects of parallel link resolution in connection graphs. PhD thesis, Department of Computer Science, Colorado State University, 1985.

    Google Scholar 

  12. R. Loganantharaj and R. A. Mueller. Parallel algorithms for obtaining solution unifiers in connection graph theorem proving. To be submitted for publication, April 1986.

    Google Scholar 

  13. R. Loganantharaj, R. A. Mueller, and R. R. Oldehoeft. Connection graph refutation: aspects of AND-parallelism. Technical Report CS-85-10, Department of Computer Science, Colorado State University, 1985.

    Google Scholar 

  14. R. Loganantharaj, R. A. Mueller, and R. R. Oldehoeft. Some theoretical and implementational aspects of Dcdp-parallelism in connection graph refutation. Technical Report CS-85-9, Department of Computer Science, Colorado State University, 1985.

    Google Scholar 

  15. D. W. Loveland. Automated Theorem Proving: a Logical Basis. North Holland Publishing Company, New York, 1978.

    Google Scholar 

  16. A. Martelli and U. Montanari. An efficient unification algorithm. TOPLAS, 4:258–282, 1982.

    Article  Google Scholar 

  17. B. Meltzer. Theorem proving for computers: some results on resolutions and renaming. Computer J., 8:341–343, January 1966.

    Google Scholar 

  18. R. R. Oldehoeft and S. J. Allan. Execution support for hep sisal. In J. S. Kowalik, editor, Parallel MIMD Computation: The HEP Supercomputer and its Applications, MIT Press, Cambridge, MA, 1985.

    Google Scholar 

  19. T. Pietrzykowski and S. Matwin. Exponential improvement of efficient backtracking. In 6 th Conference on Automated Deduction, Lecture Notes in Computer Science, 138, pages 223–239, Springer-Verlag, 1982.

    Google Scholar 

  20. J. A. Robinson. A machine oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, January 1965.

    Article  Google Scholar 

  21. Seki-Projekt. The Markgraf Carl refutation procedure. Technical Report Memo-SEKI-MK-84-01, Institut fuer Informatik I, Universitat Karlsruhe, West Germany, 1984.

    Google Scholar 

  22. Seki-Projekt. The Markgraf Carl refutation procedure: the logic engine. Technical Report Nr. 24/82, Institut fuer Informatik I, Universitat Karlsruhe, West Germany, 1982.

    Google Scholar 

  23. J. Siekmann and W. Stephan. Completeness and consistency of the connection graph proof procedure. Technical Report Nr. 7/76, Institut fuer Informatik I, Universitat Karlsruhe, West Germany, 1976.

    Google Scholar 

  24. L. Wos. Solving open questions with an automated theorem proving. In Proc. 6th conference on Automated deduction, Lecture Notes in Computer Science 138, pages 1–31, Springer-Verlag, New York, 1982.

    Google Scholar 

  25. L. Wos, D. F. Carson, and G. A. Robinson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12:687–697, 1965.

    Article  Google Scholar 

  26. L. Wos, D. F. Carson, and G. A. Robinson. The unit preference strategy in theorem proving. In Proceedings of the Fall Joint Computer Conference, Thompson Book Company, New York, 1964.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Center for Advanced Computer Studies USL, P.O. Box 44330, 70504-4330, Lafayette, LA

    Rasiah Loganantharaj

  2. Department of Computer Science, Colorado State University, 80523, Fort Collins, Colorado

    Robert A. Mueller

Authors
  1. Rasiah Loganantharaj
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert A. Mueller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jörg H. Siekmann

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Loganantharaj, R., Mueller, R.A. (1986). Parallel theorem proving with connection graphs. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_101

Download citation

  • DOI: https://doi.org/10.1007/3-540-16780-3_101

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16780-8

  • Online ISBN: 978-3-540-39861-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics