{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T11:00:38Z","timestamp":1775818838774,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540518389","type":"print"},{"value":"9783642751820","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/978-3-642-75182-0_51","type":"book-chapter","created":{"date-parts":[[2011,12,5]],"date-time":"2011-12-05T23:49:27Z","timestamp":1323128967000},"page":"527-539","source":"Crossref","is-referenced-by-count":1,"title":["P A R T H E O: A Parallel Inference Machine"],"prefix":"10.1007","author":[{"given":"S.","family":"Bayerl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Letz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Schumann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"51_CR1","unstructured":"Parallel C \u2014 User Guide. 3L Ltd., Livingston, Scotland, 1988."},{"key":"51_CR2","volume-title":"D16 \/ full first order logic parallel inference machine \u2014 language and design","author":"S Bayerl","year":"1989","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 (to appear ), 1989."},{"key":"51_CR3","volume-title":"Proceedings of the Seventh International Joint Conference on Arificial Intelligence","author":"K Bl\u00e4sius","year":"1981","unstructured":"K. Bl\u00e4sius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, and C. Walther. The Markgraf Karl refutation proof procedure. In Proceedings of the Seventh International Joint Conference on Arificial Intelligence, Vancouver, 1981."},{"key":"51_CR4","volume-title":"The Foundations of Mathematic","author":"EW Beth","year":"1959","unstructured":"E.W. Beth. The Foundations of Mathematic. North Holland, 1959."},{"key":"51_CR5","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."},{"key":"51_CR6","volume-title":"PARTHEO\/5: Layout and Design of Full First Order Logic Parallel Inference Machine","author":"S Bayerl","year":"1988","unstructured":"S. Bayerl, R. Letz, F. Kurfess, and J. Schumann. PARTHEO\/5: Layout and Design of Full First Order Logic Parallel Inference Machine. ESPRIT 415F Deliverable D14, 1988."},{"key":"51_CR7","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C-L Chang","year":"1973","unstructured":"C.-L. Chang and R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Orlando et al., 1973."},{"key":"51_CR8","volume-title":"Information Processing","author":"J Corbin","year":"1983","unstructured":"J. Corbin and Bidoit M. A Rehabilitation of Robinson\u2019s Unification Algorithm. In Information Processing. North-Holland, 1983."},{"key":"51_CR9","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. Petkoff, editore, AIMSA: Artificial Intelligence Methodology Systems Applications, Varna, Bulgaria, 1985. North-Holland."},{"key":"51_CR10","volume-title":"Entwurf eines Parallelen Theorembeweisers und dessen Simulation","author":"S Heilmeier","year":"1988","unstructured":"S. Heilmeier. Entwurf eines Parallelen Theorembeweisers und dessen Simulation. Master\u2019s thesis, Technical University Munich, 1988."},{"key":"51_CR11","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"RE Korf","year":"1985","unstructured":"R.E. Korf. Depth-first Iterative Deepening: an Optimal Admissible Tree Search. Artificial Intelligence, 27: 97\u2013109, 1985.","journal-title":"Artificial Intelligence"},{"key":"51_CR12","volume-title":"SETHEO - A High- Performance Theorem Prover","author":"R Letz","year":"1989","unstructured":"R. Letz, S. Bayerl, J. Schumann, and W. Bibel. SETHEO - A High- Performance Theorem Prover. (to appear in Journal of Automated Reasoning ), 1989."},{"key":"51_CR13","volume-title":"Automated Theorem Proving: a Logical Basis","author":"DW Loveland","year":"1978","unstructured":"D.W. Loveland. Automated Theorem Proving: a Logical Basis. North- Holland, 1978."},{"key":"51_CR14","volume-title":"Global Variables in Logic Programming","author":"R Letz","year":"1988","unstructured":"R. Letz and J. Schumann. Global Variables in Logic Programming. Technical report, ATP-Report, Technische Universita\u00e4t M\u00fcnchen, 1988."},{"key":"51_CR15","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BF03037324","volume":"2","author":"DA 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":"51_CR16","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robison","year":"1965","unstructured":"J. A. Robison. A Machine-oriented Logic Based on the Resolution Principle. Journal of the ACM, 12: 23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"51_CR17","volume-title":"SETHEO: Users Manual","author":"J Schumann","year":"1989","unstructured":"J. Schumann. SETHEO: User\u2019s Manual. Technical report, ATP- Report Technische Universit\u00e4t M\u00fcnchen, 1989."},{"key":"51_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"RM Smullyan","year":"1968","unstructured":"R.M. Smullyan. First Order Logic. Springer, 1968."},{"key":"51_CR19","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"MA 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":"51_CR20","volume-title":"7th Internation Workshop of Expert Systems and Applications","author":"J Vlahavas","year":"1987","unstructured":"J. Vlahavas and C. Halatsis. A new abstract Prolog instruction set. In 7th Internation Workshop of Expert Systems and Applications, Avignon, 1987."},{"key":"51_CR21","volume-title":"An Abstract PROLOG Instruction Set","author":"DHD Warren","year":"1983","unstructured":"D.H.D Warren. An Abstract PROLOG Instruction Set. Technical report, SRI, Menlo Park, CA, USA, 1983."},{"key":"51_CR22","first-page":"92","volume-title":"International Symposion on Logic Programming","author":"DH Warren","year":"1987","unstructured":"D. H. Warren. The SRI model for OR-parallel execution of prolog- abstract design and implementation issues. In International Symposion on Logic Programming, pages 92\u2013102, 1987."}],"container-title":["Informatik-Fachberichte","Wissensbasierte Systeme"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-75182-0_51.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T21:36:34Z","timestamp":1606253794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-75182-0_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540518389","9783642751820"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-75182-0_51","relation":{},"ISSN":["0343-3005"],"issn-type":[{"value":"0343-3005","type":"print"}],"subject":[],"published":{"date-parts":[[1989]]}}}