Partheo: A parallel inference machine ESPRIT 415 subproject F

  • W. Ertel
  • F. Kurfeß
  • R. Letz
  • X. Pandolfi
  • J. Schumann
Project 415 Presentations
Part of the Lecture Notes in Computer Science book series (LNCS, volume 365)


The work of subproject F on FP2 as a language for functional and parallel programming as well as on LCM as a parallel inference system has led to remarkable results; with FP2 a development tool for parallel systems is available which can be used for the specification and implementation of parallel systems composed of networks of processes. SETHEO, the sequential implementation of a theorem prover in the LCM part provides a full first order logic evaluation mechanism with an efficiency comparable to fast Prologs; in addition, it has been designed in a way that it also serves as the core of PARTHEO, which in its first stage mainly uses OR-parallelism to achieve further performance gain. In total, considering the technical results together with the acquired knowledge and experience, the cooperation between Nixdorf Computer AG, Paderborn, LIFIA-IMAG, Grenoble, and the Artificial Intelligence Group from the Technical University, Munich, produced a lot of beneficial interaction within and beyond the limits of the subproject.


Parallel System Transition Rule Proof Tree Communication Unit Abstract Data Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Ada 1980]
    Ada Reference manual for the ADA programming language. United States Department of Defense, 1980.Google Scholar
  2. [Backus 1978]
    Backus, J. W. Can programming be liberated from the Von Neumann style? A functional style and its algebra of programs. Comm. ACM 21(8), 1978.Google Scholar
  3. [Bayerl, Ertel, Kurfeß, Letz & Schumann 1988]
    Bayerl, S., Ertel, W., Kurfess, F., Letz, R., & Schumann, J. Layout and Design of Full First Order Logic Parallel Inference Machine. Deliverable D14, ESPRIT 415 F, 1988.Google Scholar
  4. [Belmesk 1988]
    Belmesk, Z. Méthodologie de spécification et de programmation des protocoles de communication avec le langage FP2. Cas étudié: le niveau liaison du protocole X25. Research Report LIFIA 86 — IMAG 748. Univ. Grenoble, October 1988.Google Scholar
  5. [Bibel 1987]
    Bibel, W.Automated Theorem Proving (2nd. ed.). Vieweg, Braunschweig, 1987.Google Scholar
  6. [Bibel 1983]
    Bibel, W. Matings in Matrices. Comm. of the ACM, 26, 844–852, 1983.CrossRefGoogle Scholar
  7. [Bibel, Kurfeß & al.]
    Bibel, W., Kurfess, F., Aspetsberger, K., Hintenaus, P. & J. Schumann. Parallel Inference Machines. in [Treleaven & Vanneschi 1987], 185–226, 1987.Google Scholar
  8. [Devienne & Lebegue 1986]
    Devienne, Ph. & Lebegue, P. Weighted graphs: a tool for logic programming. In Proc. CAAP 86, Nice, Lecture Notes in Computer Science 214, Springer-Verlag, March 1986.Google Scholar
  9. [Ehrich 1982]
    Ehrich, H.D. On the theory of specification, implementation and parametrization of abstract data types. Journal of the ACM 29(1), 1982.Google Scholar
  10. [Ehrig & al. 1984]
    Ehrig, H., Kreowski, H.J., Thatcher, J., Wagner, E. & Wright, J. Parameter passing in algebraic specification languages. Theoretical Computer Science 28, 1984.Google Scholar
  11. [Guttag & Horning 1978]
    Guttag, J.V. & Horning, J.J. The algebraic specification of abstract data types. Acta Informatica 10, 1978.Google Scholar
  12. [Guttag & al. 1978]
    Guttag, Horowitz & Musser Abstract data types and software validation. Comm. ACM 21(12), 1978.Google Scholar
  13. [Hufflen 1987]
    Hufflen, J.M. Une implementation de LPG en Lisp: “Grand-Guignol”. Research Report LIFIA 60 — IMAG 654, Univ. Grenoble, March 1987.Google Scholar
  14. [Ibáñez 1988]
    Ibáñez, M.B. Parallel inferencing in first order logic based on the connection method. In Proc. AIMSA 88 Conf., Varna, September 1988.Google Scholar
  15. [Jorrand 1986]
    Jorrand, Ph. Term rewriting as a basis for the design of a functional and parallel programming language. A case study: the language FP2. In ACAI 85, Lecture Notes in Computer Science 232, Springer-Verlag, 1986.Google Scholar
  16. [Jorrand 1987]
    Jorrand, Ph. Design and implementation of a parallel inference machine for first order logic: an overview. In Proc. PARLE 87, Vol I: Parallel Architectures, Eindhoven, Lecture Notes in Computer Science 258, Springer-Verlag, June 1987.Google Scholar
  17. [Jorrand & Schnoebelen 1989]
    Jorrand, Ph. & Schnoebelen, Ph. LIFIA/IMAG, Grenoble. 1989.Google Scholar
  18. [Keller 1976]
    Keller, R.M. Formal verification of parallel programs. Comm. ACM 19(7), 1976.Google Scholar
  19. [Kowalski 1983]
    Kowalski, R. Logic programming. Information Processing '83, 133–145, 1983.Google Scholar
  20. [Kurfeß 1988]
    Kurfess, F. Logic and Reasoning with Neural Models. Institut für Informatik, Technische Universität, München, 1988.Google Scholar
  21. [Letz, Schumann & Bayerl 1988]
    Letz, R., Schumann, J., and S. Bayerl. SETHEO: A SEquential THEOrem-prover for first order logic. Institut für Informatik, Techn. Universität München, München, 1988.Google Scholar
  22. [Levi 1986]
    Levi, G. Logic Programming: The Foundations, the Approach, and the Role of Concurrency. In De Bakker, J.W., De Roever, W.P., and Rozenberg, G. (eds.): Current Trends in Concurrency, LNCS 224, 396–441, Springer, 1986.Google Scholar
  23. [Marty 1987a]
    Marty, J.C. EDIT-FP2 User's Guide. Document Deliverable D9 (Part IIa) of Subproject F of ESPRIT Project 415, LIFIA, Univ. Grenoble, April 1987.Google Scholar
  24. [Marty 1987b]
    Marty, J.C. EDIT-FP2 System Programmer's Guide. Document Deliverable D8 (Part II) of Subproject F of ESPRIT Project 415, LIFIA, Univ. Grenoble, April 1987.Google Scholar
  25. [Marty & al. 1987]
    Marty, J.C., Rogé, S., Schnoebelen, Ph. Structure of the FP2 environment including the extensions. Document Deliverable D8 (Part I) of Subproject F of ESPRIT Project 415, LIFIA, Univ. Grenoble, April 1987.Google Scholar
  26. [Milner 1980]
    Milner, R. A Calculus of Communicating Processes. Lecture Notes in Computer Science 92, 1980.Google Scholar
  27. [Pandolfi 1989]
    Pandolfi, X. A distributed implementation of the FP2 communication mechanism. Manuscript LIFIA/IMAG, 1989.Google Scholar
  28. [Pereira 1984]
    Pereira, J.M. Processus communicants; un langage formel et ses modèles. Problèmes d'analyse. Thèse de 3eme cycle, Univ. Grenoble, 1984.Google Scholar
  29. [Rogé 1986]
    Rogé, S. Comparaison des comportements des processus communicants. Application au langage FP2. Thèse de Doctorat, I.N.P. Grenoble, November 1986.Google Scholar
  30. [Rogé 1988]
    Rogé, S. A parallel FP2 interpreter. ESPRIT Conference 1988.Google Scholar
  31. [Schaefer & Schnoebelen 1986]
    Schaefer, P. & Schnoebelen, Ph. Specification of a pipelined event driven simulator. Research Report LIFIA 65 — IMAG 682, Univ. Grenoble, 1986.Google Scholar
  32. [Schnoebelen 1985]
    Schnoebelen, Ph. The semantics of concurrency in FP2. Research Report LIFIA 30 — IMAG 558, Univ. Grenoble, October 1985.Google Scholar
  33. [Schnoebelen 1986a]
    Schnoebelen, Ph.μFP2: A prototype interpreter for FP2. Research Report LIFIA 41 — IMAG 573, Univ. Grenoble, January 1986.Google Scholar
  34. [Schnoebelen 1986b]
    Schnoebelen, Ph. About the implementation of FP2. Research Report LIFIA 42 — IMAG 574, Univ. Grenoble, January 1986.Google Scholar
  35. [Schnoebelen 1987]
    Schnoebelen, Ph. Rewriting techniques for the temporal analysis of communicating processes. Research Report IMAG 672, Univ. Grenoble, July 1987.Google Scholar
  36. [Schnoebelen 1988]
    Schnoebelen, Ph. Refined compilation of pattern-matching for functional languages. Research Report LIFIA 71 — IMAG 715, Univ. Grenoble, April 1988. To appear in Science of Computer Programming.Google Scholar
  37. [Schumann, Ertel & Suttner 1988]
    Schumann, J., Ertel, W., & C. Suttner. Learning Heuristics for a Theorem Prover using Back Propagation. submitted to ÖGAI-89.Google Scholar
  38. [Sifakis 1982]
    Sifakis, J. A unified approach for studying the properties of transitions systems. Theoretical Computer Science 18, 1982.Google Scholar
  39. [Steele 1984]
    Steele, G.L., Jr. COMMON LISP. Digital Press, Burlington, Mass. 1984.Google Scholar
  40. [Stolcke 1988]
    A. Stolcke. Generierung natürlichsprachlicher Sätze in unifikationsbasierten Grammatiken — Ein Konnektionistischer Ansatz. Diplomarbeit, Institut für Informatik, Techn. Universität München, München, 1988.Google Scholar
  41. [Syre 1985]
    Syre, J.C. A Review of Computer Architectures for Functional and Logic Programming Systems. Tech. Report CA-09, ECRC, München, 1985.Google Scholar
  42. [Treleaven & Vanneschi 1987]
    Treleaven, P.C. & M. Vanneschi (eds.). Future Parallel Computers. LNCS 272, Springer, Berlin, 1987.Google Scholar
  43. [Warren 1983]
    WARREN, D.H.D. An Abstract Prolog Instruction Set. SRI International, Artificial Intelligence Center, Menlo Park, California, October 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • W. Ertel
    • 1
  • F. Kurfeß
    • 2
  • R. Letz
    • 2
  • X. Pandolfi
    • 3
  • J. Schumann
    • 2
  1. 1.Nixdorf Computer AGMunich
  2. 2.Institute for Computer ScienceTechnical University MunichGermany
  3. 3.LIFIA-IMAGGrenoble

Personalised recommendations