Skip to main content
SpringerLink
Log in

Exploiting parallelism in interactive theorem provers

  • Refereed Papers
  • Conference paper
  • First Online:
Book cover Theorem Proving in Higher Order Logics (TPHOLs 1998)

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

Included in the following conference series:

Abstract

This paper reports on the implementation and analysis of the MP refiner, the first parallel interactive theorem prover. The MP refiner is a shared memory multi-processor implementation of the inference engine of Nuprl. The inference engine of Nuprl is called the refiner. The MP refiner is a collection of threads operating as sequential refiners running on separate processors. Concurrent tactics exploit parallelism by spawning tactics to be evaluated by other refiner threads simultaneously. Tests conducted with the MP refiner running on a four processor Sparc shared-memory multi-processor reveal that parallelism at the inference rule level can significantly decrease the elapsed time of constructing proofs interactively.

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.

References

  1. Stuart F. Allen. A Non-type-theoretic Semantics for a Type Theoretic Language. PhD thesis, Cornell University, 1987.

    Google Scholar 

  2. Andrew W. Appel. A runtime system. Journal of Lisp and Symbolic Compuation, 3, 1990.

    Google Scholar 

  3. Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In Programming Language Implementation and Logic Programming: 3rd International Symposium, pages 1–13. Springer-Verlag, 1991.

    Google Scholar 

  4. Soumitra Bose et al. Parthenon: A parallel theorem prover for non-horn clauses. Journal of Automated Reasoning, 8:153–181, 1989.

    Google Scholar 

  5. Robert L. Constable, Stuart F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, Douglas J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs, NJ, 1986.

    Google Scholar 

  6. C. Cornes, J. Courant, J. Filliatre, G. Huet, P. Manoury, C. Munoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi, and B. Werner. The Coq Proof Assistant Reference Manual: Version 5.10. Unpublished, 1995.

    Google Scholar 

  7. William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: A system description. In Eleventh Conference on Automated Deduction (CADE), volume 607 of Lecture Notes, in Computer Science, pages 701–705. Springer-Verlag, 1990.

    Google Scholar 

  8. M. J. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge Univesity Press, 1993.

    Google Scholar 

  9. Michael Gordon, Arthur Milner, and Christopher Wadsworth. Edinburgh LCF. Number 78 in Lecture Notes in Computer Science. Springer-Verlag, New York, 1979.

    Google Scholar 

  10. Paul Jackson. Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, 1995.

    Google Scholar 

  11. Matt Kaufmann. A user's manual for an interactive enhancement to the Boyer-Moore theorem prover. Technical Report 19, Computational Logic, Inc., 1988.

    Google Scholar 

  12. R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A high performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  13. Ewing L. Lusk and William W. McCune. Experiments with Roo, a paralled automated deduction system. In Parallelization in Inference Systems, number 590 in Lecture Notes in Artificial Intelligence, pages 139–162. Springer-Verlag, 1990.

    Google Scholar 

  14. W. W. McCune. OTTER 1.0 user's guide. Technical Report ANL-88-44, Argonne National Laboratory, 1989.

    Google Scholar 

  15. Robin Milner, Mads Tofte, and Robert Harper. The Definition Of Standard ML. MIT Press, Cambridge, MA, 1990.

    Google Scholar 

  16. J. Gregory Morrisett and Andrew Tolmach. Procs and locks: A portable multiproceessing platform for standard ml of new jersey. In Proceedings of the Fourth ACM SIGPLAN Symposium on Principles of Practice of Parallel Programming, pages 198–207. ACM, 1994.

    Google Scholar 

  17. Roderick Moten. Concurrent Refinement in Nuprl. PhD thesis, Cornell University, 1997.

    Google Scholar 

  18. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Eleventh International Conference on Automated Deduction (CADE), number 607 in Lecture Notes in Artificial Intelligence, pages 748–752. Springer Verlag, 1992.

    Google Scholar 

  19. Larry Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, Cambridge, 1987.

    Google Scholar 

  20. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1994.

    Google Scholar 

  21. Lawrence C. Paulson. ML for the Working Programmer (Second Edition). Cambridge University Press, Cambridge, 1996.

    Google Scholar 

  22. J. Schumann and R. Letz. Partheo: A high-performance parallel theorem prover. In Tenth International Conference on Automated Deduction (CADE), number 449 in Lecture Notes in Artificial Intelligence, pages 40–56. Springer-Verlag, 1990.

    Google Scholar 

  23. Johann M. Ph. Schumann. Parallel theorem provers: An overview. In Parallelization in Inference Systems, number 590 in Lecture Notes in Artificial Intelligence, pages 26–50. Springer-Verlag, 1990.

    Google Scholar 

  24. John K. Slaney and Ewing L. Lusk. Parallelizing the closure computation in automated deduction. In Tenth International Conference on Automated Deduction (CADE), number 449 in Lecture Notes in Artificial Intelligence, pages 28–39. Springer Verlag, 1990.

    Google Scholar 

  25. Christian B. Suttner. A parallel theorem prover with heuristic work distribution. In Parallelization in Inference Systems, number 590 in Lecture Notes In Computer Science, pages 243–253. Springer Verlag, 1992.

    Google Scholar 

  26. Christian B. Suttner. Parallelization of Search-based Systems by Static Partitioning with Slackness. PhD thesis, Institut für Informatik, TU München, 1995.

    Google Scholar 

  27. Christian B. Suttner and Manfred B Jobmann. Simulation analysis of static partitioning with slackness. In Parallel Processing for Artificial Intelligence 2, number 15 in Machine Intelligence and Pattern Recognition, pages 93–105. North-Holland, 1994.

    Google Scholar 

  28. Christian B. Suttner and Johann Schumann. Parallel automated theorem proving. In Parallel Processing for Artificial Intelligence 1, number 14 in Machine Intelligence and Pattern Recognition, pages 209–257. North-Holland, 1994.

    Google Scholar 

  29. D. H. D. Warren. The SRI model for OR-parallel execution of Prolog: Abstract design and implementation issues. In International Symposium on Logic Programming, pages 92–102. North-Holland, 1987.

    Google Scholar 

  30. G.A. Wilson and J. Minker. Resolution, refinements, and search strategies: A comparative study. IEEE Transactions on Computers, C-25:782–801, 1976.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Colgate University, 13224, Hamilton, NY, USA

    Roderick Moten

Authors
  1. Roderick Moten
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jim Grundy Malcolm Newey

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Moten, R. (1998). Exploiting parallelism in interactive theorem provers. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055144

Download citation

  • DOI: https://doi.org/10.1007/BFb0055144

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-49801-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation