{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:46Z","timestamp":1749124066673},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055144","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"315-330","source":"Crossref","is-referenced-by-count":4,"title":["Exploiting parallelism in interactive theorem provers"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Moten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"unstructured":"Stuart F. Allen. A Non-type-theoretic Semantics for a Type Theoretic Language. PhD thesis, Cornell University, 1987.","key":"19_CR1"},{"doi-asserted-by":"crossref","unstructured":"Andrew W. Appel. A runtime system. Journal of Lisp and Symbolic Compuation, 3, 1990.","key":"19_CR2","DOI":"10.1007\/BF01807697"},{"doi-asserted-by":"crossref","unstructured":"Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In Programming Language Implementation and Logic Programming: 3rd International Symposium, pages 1\u201313. Springer-Verlag, 1991.","key":"19_CR3","DOI":"10.1007\/3-540-54444-5_83"},{"key":"19_CR4","first-page":"153","volume":"8","author":"S. Bose","year":"1989","unstructured":"Soumitra Bose et al. Parthenon: A parallel theorem prover for non-horn clauses. Journal of Automated Reasoning, 8:153\u2013181, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR5","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"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."},{"unstructured":"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.","key":"19_CR6"},{"doi-asserted-by":"crossref","unstructured":"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\u2013705. Springer-Verlag, 1990.","key":"19_CR7","DOI":"10.1007\/3-540-55602-8_207"},{"unstructured":"M. J. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge Univesity Press, 1993.","key":"19_CR8"},{"key":"19_CR9","volume-title":"Number 78 in Lecture Notes in Computer Science","author":"M. Gordon","year":"1979","unstructured":"Michael Gordon, Arthur Milner, and Christopher Wadsworth. Edinburgh LCF. Number 78 in Lecture Notes in Computer Science. Springer-Verlag, New York, 1979."},{"unstructured":"Paul Jackson. Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, 1995.","key":"19_CR10"},{"unstructured":"Matt Kaufmann. A user's manual for an interactive enhancement to the Boyer-Moore theorem prover. Technical Report 19, Computational Logic, Inc., 1988.","key":"19_CR11"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A high performance theorem prover. Journal of Automated Reasoning, 8:183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"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\u2013162. Springer-Verlag, 1990.","key":"19_CR13","DOI":"10.1007\/3-540-55425-4_6"},{"unstructured":"W. W. McCune. OTTER 1.0 user's guide. Technical Report ANL-88-44, Argonne National Laboratory, 1989.","key":"19_CR14"},{"key":"19_CR15","volume-title":"The Definition Of Standard ML","author":"R. Milner","year":"1990","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition Of Standard ML. MIT Press, Cambridge, MA, 1990."},{"doi-asserted-by":"crossref","unstructured":"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\u2013207. ACM, 1994.","key":"19_CR16","DOI":"10.1145\/173284.155353"},{"unstructured":"Roderick Moten. Concurrent Refinement in Nuprl. PhD thesis, Cornell University, 1997.","key":"19_CR17"},{"doi-asserted-by":"crossref","unstructured":"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\u2013752. Springer Verlag, 1992.","key":"19_CR18","DOI":"10.1007\/3-540-55602-8_217"},{"key":"19_CR19","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and Computation: Interactive Proof with Cambridge LCF","author":"L. Paulson","year":"1987","unstructured":"Larry Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, Cambridge, 1987."},{"key":"19_CR20","volume-title":"Number 828 in Lecture Notes in Computer Science","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1994."},{"key":"19_CR21","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the Working Programmer","author":"L. C. Paulson","year":"1996","unstructured":"Lawrence C. Paulson. ML for the Working Programmer (Second Edition). Cambridge University Press, Cambridge, 1996.","edition":"Second Edition"},{"doi-asserted-by":"crossref","unstructured":"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\u201356. Springer-Verlag, 1990.","key":"19_CR22","DOI":"10.1007\/3-540-52885-7_78"},{"doi-asserted-by":"crossref","unstructured":"Johann M. Ph. Schumann. Parallel theorem provers: An overview. In Parallelization in Inference Systems, number 590 in Lecture Notes in Artificial Intelligence, pages 26\u201350. Springer-Verlag, 1990.","key":"19_CR23","DOI":"10.1007\/3-540-55425-4_2"},{"doi-asserted-by":"crossref","unstructured":"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\u201339. Springer Verlag, 1990.","key":"19_CR24","DOI":"10.1007\/3-540-52885-7_77"},{"doi-asserted-by":"crossref","unstructured":"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\u2013253. Springer Verlag, 1992.","key":"19_CR25","DOI":"10.1007\/3-540-55425-4_12"},{"unstructured":"Christian B. Suttner. Parallelization of Search-based Systems by Static Partitioning with Slackness. PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1995.","key":"19_CR26"},{"doi-asserted-by":"crossref","unstructured":"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\u2013105. North-Holland, 1994.","key":"19_CR27","DOI":"10.1016\/B978-0-444-81837-9.50012-9"},{"doi-asserted-by":"crossref","unstructured":"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\u2013257. North-Holland, 1994.","key":"19_CR28","DOI":"10.1016\/B978-0-444-81704-4.50015-6"},{"unstructured":"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\u2013102. North-Holland, 1987.","key":"19_CR29"},{"key":"19_CR30","doi-asserted-by":"crossref","first-page":"782","DOI":"10.1109\/TC.1976.1674697","volume":"C-25","author":"G.A. Wilson","year":"1976","unstructured":"G.A. Wilson and J. Minker. Resolution, refinements, and search strategies: A comparative study. IEEE Transactions on Computers, C-25:782\u2013801, 1976.","journal-title":"IEEE Transactions on Computers"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055144","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T02:58:35Z","timestamp":1683514715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055144"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/bfb0055144","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}