{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T09:03:53Z","timestamp":1760346233413},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_78","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:46:10Z","timestamp":1330188370000},"page":"40-56","source":"Crossref","is-referenced-by-count":32,"title":["Partheo: A high-performance parallel theorem prover"],"prefix":"10.1007","author":[{"given":"J.","family":"Schumann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Letz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"4_CR1","volume-title":"User Guide","author":"C Parallel","year":"1988","unstructured":"Parallel C \u2014 User Guide. 3L Ltd., Livingston, Scotland, 1988."},{"key":"4_CR2","unstructured":"Owen Astrachan. METEOR: Model elimination theorem prover for efficient OR-parallelism. In W.W. Bledsoe, M. Stickel, P. Lincoln, R. Overbeek, and D. Plaisted, editors, 1989 AAAI Spring Symposium on Representation and Compilation in High Performance Theorem Proving: Titles and Abstracts, Stanford, CA, 3 1989."},{"key":"4_CR3","first-page":"764","volume-title":"CADE 9","author":"P.E. Allen","year":"1988","unstructured":"P.E. Allen, S. Bose, E.M. Clarke, and S. Michaylov. PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. In CADE 9, pages 764\u2013765, Argonne, Illinois,USA, Springer, 1988."},{"key":"4_CR4","volume-title":"FGCS","author":"U. Baron","year":"1988","unstructured":"U. Baron, J. C. de Kergommeaux, M. Hailperin, M. Ratcliffe, M. Robert, J.-Cl. Syre, and H. Westphal. The parallel ECRC Prolog System PEPSys: An Overview and Evaluation Results. In FGCS, ECRC Munich, 1988."},{"key":"4_CR5","unstructured":"S. Bayerl, W. Ertel, M. v. d. Koelen, F. Kurfess, R. Letz, J. Schumann, Ch. Suttner, and N. Trapp. PARTHEO\/6: PARallel Automated THEorem Prover based on the Connection Method for Full First Order Logic \u2014 Implementation and Performance. ESPRIT 415F Deliverable D15, 1989."},{"key":"4_CR6","unstructured":"S. Bayerl, W. Ertel, F. Kurfess, R. Letz, and J. Schumann. D16 \/ Full First Order Logic PARallel Inference Machine \u2014 Language and Design. ESPRIT 415, Deliverables, Brussels, 1989."},{"key":"4_CR7","unstructured":"E.W. Beth. The Foundations of Mathematics. North-Holland, 1959."},{"key":"4_CR8","unstructured":"S. Bose, E.M. Clarke, D.E. Long, and S. Michaylov. Parthenon: A Parallel Theorem Prover for Non-Horn Clauses. In LICS, 1989."},{"key":"4_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987.","edition":"second edition"},{"issue":"5","key":"4_CR10","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1093\/comjnl\/30.5.386","volume":"30","author":"W.F. Clocksin","year":"1987","unstructured":"W.F. Clocksin. Principles of the delPhi Parallel Inference Machine. Comp. Journal, 30(5):386\u2013392, 5 1987.","journal-title":"Comp. Journal"},{"key":"4_CR11","unstructured":"J. Corbin and M. Bidoit. A Rehabilitation of Robinson's Unification Algorithm. In Information Processing, pages 909\u2013914. North-Holland, 1983."},{"key":"4_CR12","volume-title":"AIMSA: Artificial Intelligence Methodology Systems Applications","author":"E. Eder","year":"1985","unstructured":"E. Eder. An Implementation of a Theorem Prover based on the Connection Method. In W. Bibel and B. Petkoff, editors, AIMSA: Artificial Intelligence Methodology Systems Applications, Varna, Bulgaria, 1985. North-Holland."},{"key":"4_CR13","unstructured":"Ph. Jorrand and Ph. Schnoebelen. Parallel Implementation of Connection Method on an Abstract FP2 Machine. ESPRIT 415F Deliverable D17, 1989."},{"key":"4_CR14","unstructured":"V. Kumar, Y. Lin, and A. Gupta. Parallel Execution of Logic Programs. In W.W. Bledsoe, M. Stickel, P. Lincoln, R. Overbeek, and D. Plaisted, editors, 1989 AAAI Spring Symposium on Representation and Compilation in High Performance Theorem Proving: Titles and Abstracts, Stanford, CA, 3 1989."},{"key":"4_CR15","unstructured":"R. Letz and J. Schumann. Global Variables in Logic Programming. Technical report, ATP-Report, Technische Universit\u00e4t M\u00fcnchen, 1988."},{"key":"4_CR16","unstructured":"R. Letz, S. Bayerl, J. Schumann, and W. Bibel. SETHEO \u2014 A High-Performance Theorem Prover. (to appear in Journal of Automated Reasoning), 1990."},{"key":"4_CR17","unstructured":"D.W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978."},{"key":"4_CR18","unstructured":"J. Pelletier and P. Rudnicki. Non-obviousness. AAR Newsletter 6, pages 4\u20135, 1986."},{"key":"4_CR19","first-page":"710","volume-title":"CADE 9","author":"F. Pfenning","year":"1988","unstructured":"Frank Pfenning. Single Axioms in the Implicational Propositional Calculus. In CADE 9, pages 710\u2013713, Argonne, Illinois, USA, Springer, 1988."},{"key":"4_CR20","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF03037324","volume":"2","author":"D. A. Plaisted","year":"1984","unstructured":"D. A. Plaisted. The Occur-check Problem in Prolog. New Generation Computing, 2:309\u2013322, 1984.","journal-title":"New Generation Computing"},{"key":"4_CR21","unstructured":"J. Schumann, N. Trapp, and M. van der Koelen. SETHEO: User's Manual. Technical report, ATP-Report, Technische Universit\u00e4t M\u00fcnchen, 1989."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"R.M. Smullyan. First Order Logic. Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"4_CR23","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M.A. Stickel","year":"1988","unstructured":"M.A. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR24","unstructured":"J. Vlahavas and C. Halatsis. A New Abstract Prolog Instruction Set. In 7th International Workshop of Expert Systems and Applications, pages 1025\u20131050, Avignon, 1987."},{"key":"4_CR25","series-title":"Technical report","volume-title":"An Abstract PROLOG Instruction Set","author":"D.H.D Warren","year":"1983","unstructured":"D.H.D Warren. An Abstract PROLOG Instruction Set. Technical report, SRI, Menlo Park, CA, USA, 1983."},{"key":"4_CR26","unstructured":"D.H.D. Warren. Parallel Execution Models and Architectures for Prolog. Presented at Working Group Architecture, ESPRIT 415, 1 1988."},{"issue":"8","key":"4_CR27","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, 8 1976.","journal-title":"IEEE Transactions on Computers"}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_78.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:09:48Z","timestamp":1619557788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}