Skip to main content
SpringerLink
Log in

Parallel Term Rewriting with Paredux

  • Chapter
Automated Deduction — A Basis for Applications

Part of the book series: Applied Logic Series ((APLS,volume 9))

Abstract

Nowadays high performance computer architectures are parallel architectures. They can be subdivided into shared memory multiprocessors and distributed memory multiprocessors. Their most popular and commonly available representatives are shared-memory parallel workstations, and networks of workstations, respectively. Combining both kinds of architectures in the form of a network of shared memory multiprocessors results in a hierarchical multiprocessor with non-uniform memory access.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Amrhein, B., R. Bündgen, and W. Küchlin: 1998, ‘Parallel Completion Techniques’. In: M. Bronstein, J. Grabmeier, and V. Weispfenning (eds.): Proc. 1995 Workshop on Symbolic Rewriting Techniques. Monte Verità, Ascona, Switzerland. In print.

    Google Scholar 

  • Anantharaman, D. and N. Andrianarievelo: 1990, ‘Heuristical criteria in refutational theorem proving’. In: A. Miola (ed.): Design and Implementation of Symbolic Computation Systems (DISCO ‘90), Vol. 429 of Lecture Notes in Computer Science. Capri, Italy, pp. 184 – 193.

    Google Scholar 

  • Attardi, G. and C. Traverso: 1994, ‘A Strategy-Accurate parallel Buchberger algorithm’. In: H. Hong (ed.): First International Symposium on Parallel Symbolic Computation PASCO’94. pp. 12–21. (Proc. PASCO’94, Linz, Austria, September 1994 ).

    Google Scholar 

  • Avenhaus, J. and J. Denzinger: 1993, ‘Distributing Equational Theorem Proving’. In: C. Kirchner (ed.): Rewriting Techniques and Applications (LNCS 690). pp. 62–76. (Proc. RTA’93, Montreal, Canada, June 1993 ).

    Google Scholar 

  • Bachmair, L., N. Dershowitz, and D. A. Plaisted: 1989, ‘Completion Without Failure’. In: H. Aït-Kaci and M. Nivat (eds.): Rewriting Techniques, Vol. 2 of Resolution of Equations in Algebraic Structures. Academic Press, Chapt. 1.

    Google Scholar 

  • Bonacina, M. P. and J. Hsiang: 1991, ‘Completion procedures as Semidecision procedures’. In: S. Kaplan and M. Okada (eds.): Conditional and Typed Rewriting Systems (LNCS 515). pp. 206–232. (Proc. CTRS’90, Montreal, Canada, June 1990 ).

    Google Scholar 

  • Bonacina, M. P. and J. Hsiang: 1995, ‘Distributed Deduction by Clause-Diffusion: Distributed Contraction and the Acquarius Prover’. Journal of Symbolic Computation 19 (1/2/3).

    Google Scholar 

  • Bubeck, T., M. Hiller, W. Küchlin, and W. Rosenstiel: 1995, ‘Distributed Symbolic Computation with DTS’. In: A. Ferreira and J. Rolim (eds.): Parallel Algorithms for Irregularly Structured Problems, 2nd Intl. Workshop, IRREGULAR’ 95, Vol. 980 of Lecture Notes in Computer Science. Lyon, France, pp. 231 – 248.

    Google Scholar 

  • Buchberger, B., G. E. Collins, M. J. Encarnación, H. Hong, J. R. Johnson, W. Krandick, R. Loos, A. Mandache, A. Neubacher, and H. Vielhaber: 1993, ‘SACLIB User’s Guide’. Johannes Kepler Universität, 4020 Linz, Austria. Available via anonymous ftp at melmac. risc.uni-linz. ac. at in pub/saclib.

    Google Scholar 

  • Bündgen, R.: 1993, ‘Reduce the Redex ReDuX’. In: C. Kirchner (ed.): Rewriting Techniques and Applications — 5th International Conference (RTA-93), Vol. 690 of Lecture Notes in Computer Science. Montreal, Canada, pp. 446 – 450.

    Google Scholar 

  • Bündgen, R., M. Göbel, and W. Küchlin: 1994a, ‘Experiments with Multi-Threaded Knuth-Bendix Completion’. Technical Report 94-05, Wilhelm-Schickard-Institut, Universität Tübingen, D-72076 Tübingen.

    Google Scholar 

  • Bündgen, R., M. Göbel, and W. Küchlin: 1994b, ‘A Fine-Grained Parallel Completion Procedure’. In: Proc. Intl. Symposium on Symbolic and Algebraic Computation (ISSAC ‘94). Oxford.

    Google Scholar 

  • Bündgen, R., M. Göbel, and W. Küchlin: 1994c, ‘Multi-Threaded AC Term Rewriting’. In: H. Hong (ed.): First International Symposium on Parallel Symbolic Computation PASCO’94. pp. 84–93. (Proc. PASCO’94, Linz, Austria, September 1994 ).

    Google Scholar 

  • Bündgen, R., M. Göbel, and W. Küchlin: 1995, ‘Parallel ReDuX -* PaReDuX’. In: J. Hsiang (ed.): Rewriting Techniques and Applications (LNCS 914). pp. 408–413. (Proc. RTA’95, Kaiserslautern, Germany, April 1995 ).

    Google Scholar 

  • Bündgen, R., M. Göbel, and W. Küchlin: 1996a, ‘A Master-Slave Approach to Parallel Term Rewriting on a Hierachical Multiprocessor’. In: J. Calmet and C. Limongelli (eds.): Design and Implementation of Symbolic Computation Systems—International Symposium DISCO ‘96, Vol. 1128 of Lecture Notes in Computer Science. Karlsruhe, Germany, pp. 184 – 194.

    Google Scholar 

  • Bündgen, R., M. Göbel, and W. Küchlin: 1996b, ‘Strategy Compliant Multi Threaded Term Completion’. Journal of Symbolic Computation 21 (4–6), 475 – 505.

    Article  Google Scholar 

  • Collins, G. E.: 1980, ‘ALDES and SAC-2 Now Available’. SIGSAM Bulletin 12 (2), 19.

    Google Scholar 

  • Cooper, E. C. and R. P. Drayes: 1988, ‘C Threads’. Technical Report CMU-CS-88154, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213.

    Google Scholar 

  • Denzinger, J.: 1993, ‘Teamwork: Eine Methode zum Entwurf verteilter, wissensbasierter Theorembeweiser’. Ph.D. thesis, Universität Kaiserslautern, Postfach 3049, D-67663 Kaiserslautern.

    Google Scholar 

  • Denzinger, J. and M. Fuchs: 1994, ‘Goal oriented equational theorem proving using team work’. In: B. Nebel and L. Dreschler-Fischer (eds.): KI-94: Advances in Artificial Intelligence — Proceedings of the 18th German Annual Conference on Artificial Intelligence, Vol. 861 of Lecture Notes in Artificial Intelligence. Saarbrücken, Germany, pp. 343 – 354.

    Google Scholar 

  • Denzinger, J. and J. Lind: 1996, ‘TWlib—a Library for Distributed Search Applications’. In: Proc. ICS’ 96-AI. Kaohsiung, pp. 101-108.

    Google Scholar 

  • Denzinger, J. and S. Schulz: 1996, ‘Recording and Analyzing Knowledge-Based Distributed Deduction Processes’. Journal of Symbolic Computation 21, 523 – 541.

    Article  Google Scholar 

  • Dershowitz, N. and J.-P. Jouannaud: 1990, ‘Rewrite Systems’. In: J. van Leeuwen (ed.): Formal Models and Semantics, Vol. B of Handbook of Theoretical Computer Science. Amsterdam: Elsevier, chapter 6, pp. 243 – 320.

    Google Scholar 

  • Fleischer, J., J. Grabmeier, F. W. Hehl, and W. Küchlin (eds.): 1994, ‘Computer Algebra in Science and Engineering’. Bielefeld, Germany: Zentrum für Interdisziplinäre Forschung, World Scientific.

    Google Scholar 

  • Fronhöfer, B. and G. Wrightson (eds.): 1990, Parallelization in Inference Systems’, Vol. 590 of Lecture Notes in Artificial Intelligence. Dagstuhl Castle, Germany:, Springer-Verlag.

    Google Scholar 

  • Fuchs, M.: 1995, ‘Learning proof heuristics by adapting parameters’. Technical report, Fachbereich Informatik, Universiät Kaiserslautern, Postfach 3049, D-67663 Kaiserslautern.

    Google Scholar 

  • Geist, G. A. and V. S. Sunderam: 1991, ‘The PVM System: Supercomputer Level Concurrent Computation on a Heterogeneous Network of Workstations’. In: Sixth Annual Distributed-Memory Computer Conference. Portland, Oregon, pp. 258–261.

    Google Scholar 

  • Halstead, Jr., R. H.: 1985, ‘Multilisp: A Language for Concurrent Symbolic Computation’. ACM Transactions on Programming Languages and Systems 7(4), 501–538.

    Google Scholar 

  • Hsiang, J. and M. Rusinowitch: 1987, ‘On Word Problems in Equational Theories’. In: T. Ottmann (ed.): Automata, Languages and Programming (LNCS 267). pp. 54–71. (Proc. ICALP’ 87, Karlsruhe, Germany, July 1987 ).

    Google Scholar 

  • Huet, G.: 1981, ‘A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm’. Journal of Computer and System Sciences 23, 11 – 21.

    Article  Google Scholar 

  • Ito, T. and R. Halstead, Jr. (eds.): 1990, ‘US/Japan Workshop on Parallel Lisp’, Vol. 441 of Lecture Notes in Computer Science. Sendai, Japan:, Springer-Verlag.

    Google Scholar 

  • Knuth, D. E. and P. B. Bendix: 1970, ‘Simple Word Problems in Universal Algebra’. In: J. Leech (ed.): Computational Problems in Abstract Algebra. (Proc. of a conference held in Oxford, England, 1967 ).

    Google Scholar 

  • Küchlin, W.: 1982, ‘A Theorem-Proving Approach to the Knuth-Bendix Completion Algorithm’. In: J. Calmet (ed.): Computer Algebra (Proc. EUROCAM’82, LNCS 144 ).

    Google Scholar 

  • Küchlin, W.: 1985, ‘A Confluence Criterion Based on the Generalised Newman Lemma’. In: B. F. Caviness (ed.): Eurocal’85 (LNCS 204). pp. 390–399. (Proc. Eurocal’85, Linz, Austria, April 1985 ).

    Google Scholar 

  • Küchlin, W.: 1986, ‘A Generalized Knuth-Bendix Algorithm’. Technical Report 8601, Mathematics, Swiss Federal Institute of Technology (ETH), CH-8092 Zürich, Switzerland.

    Google Scholar 

  • Küchlin, W.: 1990a, ‘The S-Threads Environment for Parallel Symbolic Computation’. In: R. E. Zippel (ed.): Second International Workshop on Computer Algebra and Parallelism, Vol. 584 of Lecture Notes in Computer Science. Ithaca, USA, pp. 1 – 18.

    Google Scholar 

  • Küchlin, W. W.: 1990b, ‘PARSAC-2: A Parallel SAC-2 Based on Threads’. In: S. Sakata (ed.): Applied Algebra, Algebraic Algorithms, and Error-Correcting Codes: 8th International Conference, AAECC-8, Vol. 508 of LNCS. Tokyo, Japan, pp. 341 – 353.

    Google Scholar 

  • Küchlin, W. W.: 1995, ‘PARSAC-2: Parallel Computer Algebra on the Desk-Top’. in (Fleischer et al., 1994 ), pp. 24 – 43.

    Google Scholar 

  • Küchlin, W. W. and N. J. Nevin: 1991, ‘On Multi-Threaded List-Processing and Garbage Collection’. In: Proc. Third IEEE Symp. on Parallel and Distributed Processing. Dallas, TX, pp. 894 – 897.

    Google Scholar 

  • Küchlin, W. W. and J. A. Ward: 1992, ‘Experiments with Virtual C Threads’. In: Proc. Fourth IEEE Symp. on Parallel and Distributed Processing. Dallas, TX, pp. 50 – 55.

    Google Scholar 

  • Lusk, E. L. and W. W. McCune: 1990, ‘Experiments with ROO, A Parallel Automated Deduction System’. in (Fronhöfer and Wrightson, 1990 ), pp. 139 – 162.

    Google Scholar 

  • Lusk, E. L. and R. A. Overbeek: 1985, ‘Reasoning about Equality’. Journal of Automated Reasoning 1, 209 – 228.

    Google Scholar 

  • Maier, P., M. Göbel, and R. Bündgen: 1995, ‘A Multi-Threaded Unfailing Completion’. Technical Report 95–06, Wilhelm-Schickard-Institut, Universität Tübingen, 72076 Tübingen, Germany.

    Google Scholar 

  • Mohr, E., D. A. Kranz, and R. H. Halstead, Jr.: 1991, ‘Lazy Task Creation: A Technique for Increasing the Granularity of Parallel Programs’. IEEE Transactions on Parallel and Distributed Systems 2 (3), 264 – 280.

    Article  Google Scholar 

  • Morisse, K. and G. Oevel: 1995. Oevel: 1995, ‘New Developments in MuPAD’. in (Fleischer et al., 1994 ).

    Google Scholar 

  • Schreiner, W. and H. Hong: 1993, ‘The Design of the PACLIB Kernel for Parallel Algebraic Computation’. In: J. Volkert (ed.): Parallel Computation (LNCS 734). pp. 204–218. (Second International ACPC Conference, Gmunden, Austria, October 1993 ).

    Google Scholar 

  • Schumann, J.: 1995, ‘SiCoTHEO — Simple Competive parallel Theorem Provers based on SETHEO’. In: Proc. PPAI’95, Montreal, Canada, 1995.

    Google Scholar 

  • Slaney, J. K. and E. L. Lusk: 1990, Parallelizing the Closure Computation in Automated Deduction’. In: M. E. Stickel (ed.): 10th International Conference on Automated Deduction, (CADE’90), Vol. 449 of Lecture Notes in Compter Science. Kaiserslautern, Germany, pp. 28 – 39.

    Google Scholar 

  • Sutclife, G., C. Suttner, and T. Yemenis: 1994, ‘The TPTP Problem Library’. In: A. Bundy (ed.): 12th International Conference on Automated Deduction (CADE’94). Nancy, France, pp. 252 – 266.

    Google Scholar 

  • Tanenbaum, A. S.: 1992, Modern Operating Systems. Prentice Hall.

    Google Scholar 

  • Tarski, A.: 1956, Logic, Semantics, Metamathematics. Oxford University Press.

    Google Scholar 

  • Weiser, M., A. Demers, and C. Hauser: 1989, ‘The Portable Common Runtime Approach to Interoperability’. In: 12th ACM SOSP. pp. 114–122.

    Google Scholar 

Download references

Authors
  1. Bündgen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Göbel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Küchlin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Weber
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Darmstadt University of Technology, Germany

    Wolfgang Bibel

  2. Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, 76128, Karlsruhe, Germany

    Peter H. Schmitt

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Bündgen, Göbel, Küchlin, Weber (1998). Parallel Term Rewriting with Paredux. In: Bibel, W., Schmitt, P.H. (eds) Automated Deduction — A Basis for Applications. Applied Logic Series, vol 9. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0435-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-0435-9_9

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-5051-9

  • Online ISBN: 978-94-017-0435-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation