D. Cantone
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.
- BDL89.N. Baxter, E. Dubinsky, and G. Levin. Learning discrete mathematics with iSETL. Springer-Verlag, New York, 1989. Google Scholar
Digital Library
- Ber58.C. Berge. Theorie des graphs et ses applications. Dunod, Paris, 1958.Google Scholar
- 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.Google ScholarCross Ref
- Bol79.B. Bollobas. Graph Theory: an introductory ourse. Springer Verlag, 1979.Google Scholar
- CCP89.D. Cantone, V. Cutello, and A. Policriti. Settheoretic reductions of Hilbert's tenth problem. In Proceedings of Logic and Computer Science Workshop. Lecture notes in Computer Science, 1989. To appear. Google ScholarDigital Library
- CFO89.D. Cantone, A. Ferro, and E.G. Omodeo. Computable set theory. Oxford University Press, Oxford, 1989. Google ScholarDigital Library
- CFS87.D. Cantone, A. Ferro, and J. T. Schwartz. Decision procedures for elementary sublanguages of set theory V. Multilcvel syllogistic extended by the general union operator. journal of Computer and Sysiem Sciences., 34 (l):l-18, ~gs?. Google ScholarDigital Library
- CH80.A.K. Chandra and D. Hare}. Computable queries for relational data bases. Journal of Computers and System Sciences, 21:156-178, 1980.Google ScholarCross Ref
- CM77.A.K. Chandra and P.M. Merlin. Optimal implementation of conjunctive queries in relational databases. In Proc. Ninth Annual A CM Syrup. on the Theory of Computing, pages 77-90, 1977. Google ScholarDigital Library
- Cod72.E.F. Codd. Relational completeness of data base sublanguages. In Rustin, editor, Data Base Systems, Englewood Cliffs, N.J., 1972. Prentice-Hall.Google Scholar
- COP89.D. Cantone, E. Omodeo, and A. Policriti. The Automation of Syllogistic II. Optimization and Complexity Issues. Journal of Automated Reasoning, i989. To appear. Google ScholarDigital Library
- CS89.D. Cantone and J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. XI. Multilevel syllogistic extended by some elementary map constructs. Journal of Auiomated Reasoning, 1989. To appear. Google ScholarDigital Library
- DG79.B. Dreben and W.D. Goldfarb. The decision problem. Solvable classes of quantificational formulas. Addison-Wesley Publ. Comp. Inc., Reading, Massachusetts, 1979.Google Scholar
- 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.Google Scholar
- Gol84.W.D. Goldfarb. The Godel class with identity is unsolvable. Bull. of A.M.S., 10 (1):113- 115, 1984.Google ScholarCross Ref
- Mos88.L.E. Moser. A decision procedures for unquantified formulas of graph theory. Lecture Notes in Computer Science, 310:344-357, 1988. Google ScholarDigital Library
- Mos89.L.E. Moser. Decidability of formulas in graph theory. Fundamenta Informalicae, 12(2):163- 180, 1989.Google Scholar
- PP89.F. Parlamento and A. Policriti. Decision procedures for elementary sublanguages of set theory XIII. Model graphs, reflection and decidability. Journal o/Automated Reasoning, 1989. To appear. Google ScholarDigital Library
- Sch79.W. Schoenfeld. An undecidability result for relation algebras. J. Symb. Logic, 44(1):111- 115, 1979.Google ScholarCross Ref
- SDDS86.J.T. Schwartz, R.B.K. Dewar, E. Dubinsky, and E. Schonberg. Programming with sets: An introduction to SETL. Springer-Verlag, New York, 1986. Google ScholarDigital Library
- Sup72.P. Suppes. Axiomatic set theory. Dover Publications, Inc, New York, 1972.Google Scholar
- Tar41.A. Tarski. On the calculus of relations. J. Symb. Logic, 6(3):73-89, 1941.Google ScholarCross Ref
- Tar53.A. Tarski. Some metalogical results concerning the calculus of relations. J. Symb. Logic, 18(3):188-189, 1953.Google Scholar
- Ull88.J.D. Ullman. Principles of database and Knowledge-base systems, Volumes 1,2. Computer Science Press, Rockville, Maryland, 1988. Google ScholarDigital Library
Index Terms
- A decidable fragment of the elementary theory of relations and some applications
Recommendations
Decidable Elementary Modal Logics
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer ScienceIn this paper, the modal logic over classes of structures definable by universal first-order Horn formulas is studied. We show that the satisfiability problems for that logics are decidable, confirming the conjecture from [E. Hemaspaandra and H. Schnoor,...
Decidable metric logics
The common metric temporal logic for continuous time were shown to be insufficient, when it was proved that they cannot express a modality suggested by Pnueli. Moreover no finite temporal logic can express all the natural generalizations of this ...
A fragment of ML decidable by visibly pushdown automata
ICALP'11: Proceedings of the 38th international conference on Automata, languages and programming - Volume Part IIThe simply-typed, call-by-value language, RML, may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct in the sense of Reynolds. By a short type, we mean a type of order at most 2 and ...
Comments