Distributed deduction by Clause-Diffusion: the aquarius prover

  • Maria Paola BonacinaEmail author
  • Jieh Hsiang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 722)


Aquarius is a distributed theorem prover for first order logic with equality, developed for a network of workstations. Given in input a theorem proving problem and the number n of active nodes, Aquarius creates n deductive processes, one on each workstation, which work cooperatively toward the solution of the problem. Aquarius realizes a specific variant of a general methodology for distributed deduction, which we have called deduction by Clause-Diffusion and described in full in [6]. The subdivision of the work among the processes, their activities and their cooperation are defined by the Clause-Diffusion method. Aquarius incorporates the sequential theorem prover Otter, in such a way that Aquarius implements the parallelization, according to the Clause-Diffusion methodology, of all the strategies provided in Otter.

In this paper we give first an outline of the Clause-Diffusion methodology. Next, we consider in more detail the problem of distributed global contraction, e.g. normalization with respect to a distributed data base. The Clause-Diffusion methodology comprises a number of schemes for performing distributed global contraction, which avoid the backward contraction bottleneck of purely shared memory approaches to parallel deduction. Then, we describe Aquarius, its features and we analyze some of the experiments conducted so far. We conclude with some comparison and discussion.


Shared Memory Inference Rule Forward Contraction Search Plan Expansion Step 
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. 1.
    S.Anantharaman, J.Hsiang, Automated Proofs of the Moufang Identities in Alternative Rings, JAR, Vol. 6, No. 1, 76–109, 1990.Google Scholar
  2. 2.
    A.Wasilewska, Personal communication, March 1993.Google Scholar
  3. 3.
    J.Avenhaus and J.Denzinger, Distributing Equational Theorem Proving, in C.Kirchner (ed.), Proc. of the 5th RTA Conf., Springer Verlag, LNCS, to appear.Google Scholar
  4. 4.
    W. Bledsoe, Challenge problems in elementary calculus, JAR, Vol. 6, No. 3, 341–359, 1990.Google Scholar
  5. 5.
    M.P. Bonacina, Problems in Lukasiewicz logic, Newsletter of the AAR, No. 18, 5–12, Jun. 1991.Google Scholar
  6. 6.
    M.P.Bonacina, Distributed Automated Deduction, Ph.D. Thesis, Dept. of Computer Science, SUNY at Stony Brook, Dec. 1992.Google Scholar
  7. 7.
    M.P.Bonacina and J.Hsiang, On fairness in distributed deduction, in P.Enjalbert, A.Finkel and K.W.Wagner (eds.), Proc. of the 10th STACS, Springer Verlag, LNCS 665, 141–152, 1993.Google Scholar
  8. 8.
    D.Champeaux, Sub-problem finder and instance checker: Two cooperating preprocessors for theorem provers, in Proc. of the 6th IJCAI, 191–196, 1979.Google Scholar
  9. 9.
    K.M.Chandy, S.Taylor, An Introduction to Parallel Programming, Jones and Bartlett, 1991.Google Scholar
  10. 10.
    J.D.Christian, High-Performance Permutative Completion, Ph.D. Thesis, Univ. of Texas at Austin and MCC Tech. Rep. ACT-AI-303-89, Aug. 1989.Google Scholar
  11. 11.
    S.E.Conry, D.J.MacIntosh and R.A.Meyer, DARES: A Distributed Automated REasoning System, in Proc. of the 11th AAAI Conf., 78–85, 1990.Google Scholar
  12. 12.
    J.Denzinger, Distributed knowledge-based deduction using the team-work method, Tech. Rep. SR-91-12, Univ. of Kaiserslautern, 1991.Google Scholar
  13. 13.
    I.Foster, S.Tuecke, Parallel Programming with PCN, Tech. Rep. ANL-91/32, Argonne Nat. Lab., Dec. 1991.Google Scholar
  14. 14.
    D.J.Hawley, A Buchberger Algorithm for Distributed Memory Multi-Processors, in Proc. of the International Conference of the Austrian Center for Parallel Computation, Oct. 1991, Springer Verlag, LNCS, to appear.Google Scholar
  15. 15.
    A.Jindal, R.Overbeek and W.Kabat, Exploitation of parallel processing for implementing high-performance deduction systems, JAR, Vol. 8, 23–38, 1992.Google Scholar
  16. 16.
    D.Kapur. H.Zhang, RRL: a Rewrite Rule Laboratory, in E.Lusk, R.Overbeek (eds.), Proc. of CADE-9, LNCS 310, 768–770, 1988.Google Scholar
  17. 17.
    C.Kirchner, P.Viry, Implementing Parallel Rewriting, in B.Fronhöfer and G.Wrightson (eds.), Parallelization in Inference Systems, Springer Verlag, LNAI 590, 123–138, 1992.Google Scholar
  18. 18.
    E.L.Lusk, W.W.McCune, Experiments with ROO: a Parallel Automated Deduction System, in B.Fronhöfer and G.Wrightson (eds.), Parallelization in Inference Systems, Springer Verlag, LNAI 590, 139–162, 1992.Google Scholar
  19. 19.
    W.W. McCune, L. Wos, Some Fixed Point Problems in Combinatory Logic, Newsletter of the AAR, No. 10, 7–8, Apr. 1988.Google Scholar
  20. 20.
    W.W.McCune, OTTER 2.0 Users Guide, Tech. Rep. ANL-90/9, Argonne Nat. Lab., Mar. 1990.Google Scholar
  21. 21.
    F.J. Pelletier, Seventy-five problems for testing automatic theorem provers, JAR, Vol. 2, 191–216, 1986.Google Scholar
  22. 22.
    K.Siegl, Gröbner Bases Computation in STRAND: A Case Study for Concurrent Symbolic Computation in Logic Programming Languages, M.S. Thesis and Tech. Rep. 90-54.0, RISC-LINZ, Nov. 1990.Google Scholar
  23. 23.
    M.E.Stickel, The Path-Indexing Method for Indexing Terms, Tech. Note 473, SRI Int., Oct. 1989.Google Scholar
  24. 24.
    S.Tuecke, Personal communications, May 1992 and Dec. 1992.Google Scholar
  25. 25.
    J.-P. Vidal, The Computation of Gröbner Bases on A Shared Memory Multiprocessor, in A.Miola (ed.), Proc. of DISCO90, Springer Verlag, LNCS 429, 81–90, Apr. 90 and Tech. Rep. CMU-CS-90-163, Carnegie Mellon Univ., Aug. 1990.Google Scholar
  26. 26.
    L.Wos, Automated Reasoning: 33 Basic Research Problems, Prentice Hall, 1988.Google Scholar
  27. 27.
    K.A.Yelick and S.J.Garland, A Parallel Completion Procedure for Term Rewriting Systems, in D.Kapur (ed.), Proc. of the 11th CADE, Springer Verlag, LNAI 607, 109–123, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  1. 1.Department of Computer ScienceSUNY at Stony BrookStony BrookUSA

Personalised recommendations