Modelling and Performance Analysis of a Parallel Theorem Prover

  • M. Jobmann
  • J. Schumann
Conference paper
Part of the Informatik-Fachberichte book series (INFORMATIK, volume 286)


For the evaluation of the performance of an OR-parallel theorem prover (PARTHEO)1 on a network of transputers, a technique of modelling has been used to gain insight into the migration of proof tasks, load balancing, and the utilisation of the processors. The model which will be described in this paper is a queueing network model extended with explicit process interaction and communication. It is evaluated by simulation using the software tool MAOS2. In this paper we will present the results of several experiments which show the influence of parameters upon the distribution of proof tasks over the network of processors.


Modelling techniques Queueing networks Simulation Deduction and Theorem Proving Concurrent Programming OR-parallelism 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [3L 88]
    3L Ltd.. Parallel C — User Guide,, Scotland, 1988.Google Scholar
  2. [BCLM89]
    S. Bose, E. M. Clarke, D. E. Long, and S. Michaylov. Parthenon: A Parallel Theorem Prover for Non-Horn Clauses, 1989. To appear in Journal of Automated Reasoning.Google Scholar
  3. [BEK+89]
    S. Bayerl, W. Ertel, F. Kurfess, R. Letz, and J. Schumann. D16/Full first order logic parallel inference machine - Language and Design. ESPRIT 415, Deliverable D16, Brussels, 1989.Google Scholar
  4. [Bib87]
    W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987.zbMATHGoogle Scholar
  5. [FJ89]
    R. Feix and M. R. Jobmann. MAOS — Model Analysis and Optimisation System (Version 1.0). Mitteilung Nr. 173/89, Fachbereich Informatik, Universität Hamburg, 1989.Google Scholar
  6. [Job82]
    M. R. Jobmann. ILMAOS - Eine Sprache zur Formulierung von RechensyHtemmodellen. Bericht Nr. 91, Fachbereich Informatik, Universität Hamburg, 1982.Google Scholar
  7. [Job91]
    M. R. Jobmann. Leistungsanalyse von Rechen- und Kommunikationssystemen — Konzepte der Modellauswertung und Definition einer Modellierungssprache. Dissertation, Universität Hamburg, Feb 1991.Google Scholar
  8. [KGK90]
    V. Kumar, P. S. Gopalakrishnan, and L. N. Kanal. Parallel Algorithms for Machine Intelligence and Vision. Springer Verlag, New York, 1990.CrossRefGoogle Scholar
  9. [Lov78]
    D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.Google Scholar
  10. [LSBB90]
    R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETUEO: A High-Performance Theorem Prover. Technical report, Technische Universität München, 1990. To appear in Journal of Automated Reasoning.Google Scholar
  11. [RL78]
    M. Reiser and S. S. Lavenberg. Mean value analysis of closed multichain queueing networks. Research Report RC-7023, IBM Thomas Watson Research Institute, Yorktown Heights, N. Y., March 1978.Google Scholar
  12. [Sch91]
    J. Schumann. Efficient Theorem Provers based on an Abstract Machine. Dissertation, Technische Universität, München, 1991 (in preparation).Google Scholar
  13. [SL90]
    J. Schumann and R. Letz. PARTHEO: a High Performance Parallel Theorem Prover. In CADE10. Springer, 1990.Google Scholar
  14. [Sta87]
    SIS Standardiseringsgrupp, editor. Databehandling-Programspräk - SIMULA. SIS Standardiseringskom- missionen i Sverige, 1987.Google Scholar
  15. [War83]
    D. II. D. Warren. An Abstract PROLOG Instruction Set. Technical report, SRI, Menlo Park, Ca, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • M. Jobmann
    • 1
  • J. Schumann
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchen 2Deutschland

Personalised recommendations