N-axioms Parallel Unification

• Autorzy: Bellia M. , Occhiuto M.E.
• Języki publikacji: EN

Abstrakty

EN

MGUmon and MGUk-rep have a complementary role in unification in the complexity class NC . MGUmon is the upper bound of the unification classes that fall in NC and whose inputs admit an unrestricted number of repeated variables. MGUk-rep is the upper bound of the unification classes that still fall in NC but whose inputs admit an unrestricted arity on term constructors. No LogSpace reduction of the one to the other class is known. Moreover, very fast algorithms that solve the two separately are well known but no one is able to compute with both in polylog PRAM-Time. N-axioms unification extends the structure of unification inputs and brings out the notion of interleaving variable as a special repeated variable which serializes independet computations. Based on it, we define the unification class AMGUkp/h whose inputs have a fixed number of interleaving variables but admit unrestricted number of repeated variables and, at the same time, unrestricted arity for term constructors. Constructively, we prove that AMGUkp/h is in NC by introducing a new unification algorithm that works on graph contractions and solves AMGUkp/hin a polylog PRAM time of the input size. Finally, we prove that MGUmon, MGUk-rep and MGUlinear all are LogSpace reducible to AMGUkp/h. Hence, AMGUkp/h becomes the upper bound of the unification classes that are proved to be in NC .

Słowa kluczowe

EN

N-axioms unification; PRAM algorithms; complexity classes; graph contractions; interleaving variables

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 55, nr 2
• Strony: 115--128
• Opis fizyczny: Bibliogr. 31 poz.

Twórcy

autor

Bellia M.

autor

Occhiuto M.E.

• Dipartimento di Informatica, Universita di Pisa, Via F. Buonarroti, 2, 56127 Pisa, Italy,

Bibliografia

• [1] Auger, I., M.S., K.: A parallel algorithm for the monadic unification problem, BIT, 25, 1985, 302-306.
• [2] Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: Combining decision procedures, Symbolic Computation, 21(2), 1998, 211-244.
• [3] Barklund, J.: Parallel unification, Ph.D. Thesis, Upsala University, 1990.
• [4] Bejor, R., Mania, F.: Solving Combinatorial Problems with Regular Local Search Algorithms, Proc. Of 6th LPAR’99, 1705, Springer Verlag, 1999.
• [5] Bellia, M., Occhiuto, M.: Suprema of open and closed formulas and their application to resolution, Information and Computation, 117(1), 1995, 136-150.
• [6] Bellia, M., Occhiuto, M.: Combinatorial Lazy Unification, Journal of Symbolic Computation, 27, 1999, 185-206.
• [7] Bellia, M., Occhiuto, M.: New bounds in parallel unification, Proc. Of CSP’2002, Humboldt-Universitat, Berlin, 2002.
• [8] Bodea, L.: Knowledge Modeling and Reusability in , Proc. Of 60th IJCAI’99, 1999.
• [9] Chong, K., T.W., L.: Finding Connected Components in Time on the EREW PRAM, J. of Algorithms, 18, 1995, 378-402.
• [10] Clark, K.: Logic-programming Schemes and Their Implementations, in: Essays in Honor of Alan Robinson, Computational Logic (J. L. Lassez, G. Plotkin, Eds.), MIT Press, 1991, 487-541.
• [11] Dwork, C., Kanellakis, P., Mitchell, J.: On the sequential nature of unification, J. Logic Programming, 1, 1984, 35-50.
• [12] Dwork, C., Kanellakis, P., Stockemayer, L.: Parallel algorithms for term matching, Proc. Of the Int. Conf. On Automated Deduction, 1986.
• [13] Eder, E.: Properties of Substitutions and Unification, Journal of Symbolic Computation, 1, 1985, 31-46.
• [14] Harland, J., Jaffar, J.: On Parallel Unification for Prolog, New Generation Computing, 5, 1987, 259-279.
• [15] Huet, G.: Resolution d’equations dans les language d’ordre 1,2,...,w, Ph.D. Thesis, Univ. de Paris VII, 1976.
• [16] Inoue, K., Sakama, C.: Abducing Priorities to Derive Intended Conclusions, Proc. Of 60th IJCAI’99, 1999, 44-49.
• [17] Jaja, J.: An introduction to parallel algorithms, Addison Wesley Publishing Company, 1992.
• [18] Jansson, P., Jeuring, J.: Polytypic unification, Functional Programming, 8, 1998, 527-536.
• [19] Johnson, D.: A catalog of complexity classes, in: Algorithms and Complexity (J. Leeuwen, Ed.), HandBook of Theoretical Computer Science, Elsevier Science Publisher, 1990, 67-162.
• [20] Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification, in: Formal Models and Semantics (J. Lassez, G. Plotkin, Eds.), Computational Logic: Essay in Honor of Alan Robinson, The MIT Press, 1991, 257-321.
• [21] Kanellakis, P., Reves, P.: On relationship of congruence closure and unification, J. of Symbolic Computation, 7(4), 1989, 427-44.
• [22] Karp, R., Ramachandran, V.: Parallel Algorithms for Shared-Memory Machines, in: Algorithms and Complexity (J. V. Leeuwen, Ed.), vol. A of HandBook of Theoretical Computer Science, Elsevier Science Publisher, 1990, 869-942.
• [23] Leeuwen, J.: Graph algorithms, in: Algorithms and complexity (J. Leeuwen, Ed.), HandBook of Theoretical Computer Science, Elsevier Science Publisher, 1990, 525-632.
• [24] Martelli, A., Moiso, C., Rossi, G.: An Algorithm for Unification in Equational Theories, Symposium on Logic Programming, 1986.
• [25] Martelli, A., Montanari, U.: An efficient unification algorithm, ACM Trans. on Progr. Lang. and Sys, 4(2), 1982, 259-282.
• [26] Paterson, M., Wegman, M.: Linear unification, J. Comput. Syst. Sci, 16, 1978, 158-167.
• [27] Robinson, J.: A Machine-oriented logic based on the resolution principle, J.ACM, 12, 1965, 23-41.
• [28] Robinson, P.: The SUM: an AI Coprocessor, Byte, June 1985, 169-180.
• [29] Shapiro, E.: The family of concurrent logic programming languages, Computing Surveys, 21(3), 1989, 413-510.
• [30] Vitter, S., Simon, R.: New classes in parallel complexity: A study of unification and other complete problems, IEEE Trans. Comput, 35(5), 1986.
• [31] Yasuura, H.: On parallel computational complexity of unification, Proc. Of the Intern. Conf. On the Fifth Generation Computer Systems (ICOT), 1984.
• [1] Auger, I., M.S., K.: A parallel algorithm for the monadic unification problem, BIT, 25, 1985, 302-306.
• [2] Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: Combining decision procedures, Symbolic Computation, 21(2), 1998, 211-244.
• [3] Barklund, J.: Parallel unification, Ph.D. Thesis, Upsala University, 1990.
• [4] Bejor, R., Mania, F.: Solving Combinatorial Problems with Regular Local Search Algorithms, Proc. Of 6th LPAR’99, 1705, Springer Verlag, 1999.
• [5] Bellia, M., Occhiuto, M.: Suprema of open and closed formulas and their application to resolution, Information and Computation, 117(1), 1995, 136-150.
• [6] Bellia, M., Occhiuto, M.: Combinatorial Lazy Unification, Journal of Symbolic Computation, 27, 1999, 185-206.
• [7] Bellia, M., Occhiuto, M.: New bounds in parallel unification, Proc. Of CSP’2002, Humboldt-Universitat, Berlin, 2002.
• [8] Bodea, L.: Knowledge Modeling and Reusability in , Proc. Of 60th IJCAI’99, 1999.
• [9] Chong, K., T.W., L.: Finding Connected Components in Time on the EREW PRAM, J. of Algorithms, 18, 1995, 378-402.
• [10] Clark, K.: Logic-programming Schemes and Their Implementations, in: Essays in Honor of Alan Robinson, Computational Logic (J. L. Lassez, G. Plotkin, Eds.), MIT Press, 1991, 487-541.
• [11] Dwork, C., Kanellakis, P., Mitchell, J.: On the sequential nature of unification, J. Logic Programming, 1, 1984, 35-50.
• [12] Dwork, C., Kanellakis, P., Stockemayer, L.: Parallel algorithms for term matching, Proc. Of the Int. Conf. On Automated Deduction, 1986.
• [13] Eder, E.: Properties of Substitutions and Unification, Journal of Symbolic Computation, 1, 1985, 31-46.
• [14] Harland, J., Jaffar, J.: On Parallel Unification for Prolog, New Generation Computing, 5, 1987, 259-279.
• [15] Huet, G.: Resolution d’equations dans les language d’ordre 1,2,...,w, Ph.D. Thesis, Univ. de Paris VII, 1976.
• [16] Inoue, K., Sakama, C.: Abducing Priorities to Derive Intended Conclusions, Proc. Of 60th IJCAI’99, 1999, 44-49.
• [17] Jaja, J.: An introduction to parallel algorithms, Addison Wesley Publishing Company, 1992.
• [18] Jansson, P., Jeuring, J.: Polytypic unification, Functional Programming, 8, 1998, 527-536.
• [19] Johnson, D.: A catalog of complexity classes, in: Algorithms and Complexity (J. Leeuwen, Ed.), HandBook of Theoretical Computer Science, Elsevier Science Publisher, 1990, 67-162.
• [20] Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification, in: Formal Models and Semantics (J. Lassez, G. Plotkin, Eds.), Computational Logic: Essay in Honor of Alan Robinson, The MIT Press, 1991, 257-321.
• [21] Kanellakis, P., Reves, P.: On relationship of congruence closure and unification, J. of Symbolic Computation, 7(4), 1989, 427-44.
• [22] Karp, R., Ramachandran, V.: Parallel Algorithms for Shared-Memory Machines, in: Algorithms and Complexity (J. V. Leeuwen, Ed.), vol. A of HandBook of Theoretical Computer Science, Elsevier Science Publisher, 1990, 869-942.
• [23] Leeuwen, J.: Graph algorithms, in: Algorithms and complexity (J. Leeuwen, Ed.), HandBook of Theoretical Computer Science, Elsevier Science Publisher, 1990, 525-632.
• [24] Martelli, A., Moiso, C., Rossi, G.: An Algorithm for Unification in Equational Theories, Symposium on Logic Programming, 1986.
• [25] Martelli, A., Montanari, U.: An efficient unification algorithm, ACM Trans. on Progr. Lang. and Sys, 4(2), 1982, 259-282.
• [26] Paterson, M., Wegman, M.: Linear unification, J. Comput. Syst. Sci, 16, 1978, 158-167.
• [27] Robinson, J.: A Machine-oriented logic based on the resolution principle, J.ACM, 12, 1965, 23-41.
• [28] Robinson, P.: The SUM: an AI Coprocessor, Byte, June 1985, 169-180.
• [29] Shapiro, E.: The family of concurrent logic programming languages, Computing Surveys, 21(3), 1989, 413-510.
• [30] Vitter, S., Simon, R.: New classes in parallel complexity: A study of unification and other complete problems, IEEE Trans. Comput, 35(5), 1986.
• [31] Yasuura, H.: On parallel computational complexity of unification, Proc. Of the Intern. Conf. On the Fifth Generation Computer Systems (ICOT), 1984.