1. Avenhaus, J., Denzinger, J.: Distributing equational theorem proving,to appear as SEKI-Report, Universität Kaiserslautern, 1993.

   Google Scholar 

2. Avenhaus, J., Madlener, K.: Term Rewriting and Equational Reasoning, in R.B. Banerji (ed):Formal Techniques in Artificial Intelligence, Elsevier, 1990, pp. 1–43.

   Google Scholar 

3. Antoniou, G., Ohlbach, H.J.: Terminator,Proc. 8th IJCAI, Karlsruhe, 1983.

   Google Scholar 

4. Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs,Proc. Symposium on Logic in Computer Science, 1986, pp. 346–357.

   Google Scholar 

5. Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without Failure,Coll. on the Resolution of Equations in Algebraic Structures,Austin (1987),Academic Press,1989.

   Google Scholar 

6. Bonacina, M.P., Hsiang, J.: On fairness in distributed automated deduction,to be published.

   Google Scholar 

7. Conry, S.E.; MacIntosh, D.J., Meyer, R.A.: DARES: A Distributed Automated REasoning System,Proc. AAAI-90, 1990, pp. 78–85.

   Google Scholar 

8. Denzinger, J.: TEAMWORK: A method to design distributed knowledge based equational theorem provers,forthcoming Ph.D. thesis, University of Kaiserslautern, 1993.

   Google Scholar 

9. Dershowitz, N., Jouannaud, J.P.: Rewriting systems, in J. van Leeuwen (Ed.):Handbook of theoretical computer science, Vol. B., Elsevier, 1990, pp. 241–320.

   Google Scholar 

10. Ertel, W.: Random Competition: A Simple, but Efficient Method for Parallelizing Inference Systems,Int. Report TUM-19050, Technical University of Munich, 1990.

    Google Scholar 

11. Garland, S.J., Yelick, K.A.: A Parallel Completion procedure for Term Rewriting Systems,Proc. 11th CADE, 1992, pp. 109–123.

    Google Scholar 

12. Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,Journal of ACM,Vol. 27,No. 4,1980,pp. 798–821.

    Article MathSciNet  Google Scholar 

13. Knuth, D.E., Bendix, P.B.: simple Word Problems in Universal Algebra,Computational Algebra, J. Leech, Pergamon Press, 1970, pp. 263–297.

    Google Scholar 

14. Slaney, J.K., Lusk, E.L.: Parallelizing the Closure Computation in Automated Deduction,Proc. 10th CADE,LNAI 449,Springer,Kaiserslautern,1990,pp. 28–39.

    Google Scholar 

15. Stickel, M.E.: A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x3 =x implies Ring Commutativity,Proc. CADE-7, LNCS 170, Springer, 1984, pp. 248–258.

    Google Scholar 

16. Tarski, A.: Logic, Semantics, Meta mathematics,Oxford University Press, 1956.

    Google Scholar 

Download references