A decidable fragment of the elementary theory of relations and some applications

ABSTRACT

The class of purely universal formulae of the elementary theory of relations with equality is shown to have an NP-complete satisfiability problem, under the assumption that there is an a priori bound on the length of quantifier prefixes and the arities of relation variables. In the second part of the paper we discuss possible applications in the field of theorem proving in set and graph theory and of consistency checking for queries in relational databases.

REFERENCES

• BDL89: N. Baxter , Ed Dubinsky , G. Levin, Learning Discrete Math with ISETL, Springer-Verlag New York, Inc., Secaucus, NJ, 1990
• Ber58: C. Berge. Theorie des graphs et ses applications. Dunod, Paris, 1958.
• BFOS81: M. Breban, A. Ferro, E. Omodeo, and J. T. Schwartz. Decision procedures for elementary sublanguages of set theory II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Comm. Pure App. Math., 34:177-195, 1981.
• Bol79: B. Bollobas. Graph Theory: an introductory ourse. Springer Verlag, 1979.
• CCP89: D. Cantone , V. Cutello , A. Policriti, Set-theoretic reduction of Hilbert's tenth problem, Proceedings of the third workshop on Computer science logic, p.65-75, July 1990, Kaiserslautern, Germany
• CFO89: Domenico Cantone , Alfredo Ferro , Eugenio Omodeo, Computable set theory, Clarendon Press, New York, NY, 1989
• CFS87: D. Cantone , A. Ferro , J. T. Schwartz, Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator, Journal of Computer and System Sciences, v.34 n.1, p.1-18, Feb. 1987 [doi>10.1016/0022-0000(87)90001-8]
• CH80: A.K. Chandra and D. Hare}. Computable queries for relational data bases. Journal of Computers and System Sciences, 21:156-178, 1980.
• CM77: Ashok K. Chandra , Philip M. Merlin, Optimal implementation of conjunctive queries in relational data bases, Proceedings of the ninth annual ACM symposium on Theory of computing, p.77-90, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803397]
• Cod72: E.F. Codd. Relational completeness of data base sublanguages. In Rustin, editor, Data Base Systems, Englewood Cliffs, N.J., 1972. Prentice-Hall.
• COP89: D. Cantone , E. G. Omodeo , A. Policriti, The automation of syllogistic. II. optimization and complexity issues, Journal of Automated Reasoning, v.6 n.2, p.173-187, Jun. 1990 [doi>10.1007/BF00245817]
• CS89: D. Cantone , J. T. Schwartz, Decision procedures for elementary sublanguages of set theory: XI. Multilevel syllogistic extended by some elementary map constructs, Journal of Automated Reasoning, v.7 n.2, p.231-256, June 1991
• DG79: B. Dreben and W.D. Goldfarb. The decision problem. Solvable classes of quantificational formulas. Addison-Wesley Publ. Comp. Inc., Reading, Massachusetts, 1979.
• FO78: A. Ferro and E.G. Omodeo. An efficient validity test for formulae in extensional twolevel syllogistic. Le Matemaiiche (Caiania, Italy), 33:130-137, 1978.
• Gol84: W.D. Goldfarb. The Godel class with identity is unsolvable. Bull. of A.M.S., 10 (1):113- 115, 1984.
• Mos88: Louise E. Moser, A Decision Procedure for Unquantified Formulas of Graph Theory, Proceedings of the 9th International Conference on Automated Deduction, p.344-357, May 23-26, 1988
• Mos89: L.E. Moser. Decidability of formulas in graph theory. Fundamenta Informalicae, 12(2):163- 180, 1989.
• PP89: Franco Parlamento , Alberto Policriti, Decision procedures for elementary sublanguages of set theory: XIII. Model graphs, reflection and decidability, Journal of Automated Reasoning, v.7 n.2, p.271-284, June 1991
• Sch79: W. Schoenfeld. An undecidability result for relation algebras. J. Symb. Logic, 44(1):111- 115, 1979.
• SDDS86: J. T. Schwartz , R. B. Dewar , E. Schonberg , E. Dubinsky, Programming with sets; an introduction to SETL, Springer-Verlag New York, Inc., New York, NY, 1986
• Sup72: P. Suppes. Axiomatic set theory. Dover Publications, Inc, New York, 1972.
• Tar41: A. Tarski. On the calculus of relations. J. Symb. Logic, 6(3):73-89, 1941.
• Tar53: A. Tarski. Some metalogical results concerning the calculus of relations. J. Symb. Logic, 18(3):188-189, 1953.
• Ull88: Jeffrey D. Ullman, Principles of database and knowledge-base systems, Vol. I, Computer Science Press, Inc., New York, NY, 1988

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computability theory

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Theory