Decision problems for tarski and presburger arithmetics extended with sets

  • D. Cantone
  • V. Cutello
  • J. T. Schwartz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 533)


Decision Procedure Numeric Variable Choice Function Intended Meaning Subsidiary Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Ble77]
    W.W. Bledsoe. Non-resolution theorem proving. J. Art. Int., 9:1–35, 1977.CrossRefGoogle Scholar
  2. [Ble84]
    W.W. Bledsoe. Some automatic proof in analysis. Contemporary AMS editor, Automated Theorem Proving after 25 years, 1984.Google Scholar
  3. [CFO90]
    D. Cantone, A. Ferro, and E.G. Omodeo. Computable Set Theory. Oxford University Press, 1990.Google Scholar
  4. [CFOS87]
    D. Cantone, A. Ferro, E. Omodeo, and J.T. Schwartz. Decision algorithms for some fragments of Analysis and related areas. Comm. Pure App. Math., XL:281–300, 1987.Google Scholar
  5. [CO89a]
    D. Cantone and E. Omodeo. On the decidability of formulae involving continuous and closed functions. In N.S. Sridharam, editor, Eleventh Int. Joint Conf. on Art. Intell., pages 425–430, 1989.Google Scholar
  6. [CO89b]
    D. Cantone and E. Omodeo. Topological syllogistic with continuous and closed functions. Comm. Pure App. Math., XLII, n. 8:1175–1188, 1989.Google Scholar
  7. [Col75]
    G.E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. Proc. 2nd GI Conf. Automata Theory and Formal Languages. Springer Lecture Notes in CS, 33:134–183, 1975.Google Scholar
  8. [COP90]
    D. Cantone, E. Omodeo, and A. Policriti. The automation of syllogistic. II. Optimisation and complexity issues. Journal of Automated Reasoning, 6:173–187, 1990.CrossRefGoogle Scholar
  9. [DH88]
    J.H. Davenport and J. Heintz. Real quantifier elimination is doubly exponential. J. Symb. Comp., 5:29–35, 1988.Google Scholar
  10. [DST88]
    J.H. Davenport, Y. Siret, and E. Tournier. Computer Algebra. Systems and algorithms for algebraic computation. Academic Press Limited, 1988.Google Scholar
  11. [FO87]
    A. Ferro and E. Omodeo. Decision procedures for elementary sublanguages of set theory. VII. validity in set theory when a choice operator is present. Comm. Pure App. Math., XL:265–280, 1987.Google Scholar
  12. [FOS80]
    A. Ferro, E. Omodeo, and J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. I. Multilevel syllogistic and some extensions. Comm. Pure App. Math., XXXIII:599–608, 1980.Google Scholar
  13. [GN72]
    R.S. Garfinkel and G.L. Nemhauser. Integer programming. John Wiley & Sons, Inc., New York, 1972.Google Scholar
  14. [Mat70]
    Y. Matijasevič. Enumerable sets are Diophantine sets. Soviet Math. Doklady, 11:354–357, 1970.Google Scholar
  15. [Omo84]
    E.G. Omodeo. Decidability and proof procedures for set theory with a choice operator. PhD thesis, New York University, 1984.Google Scholar
  16. [Pap81]
    C.H. Papadimitriou. On the complexity of Integer Programming. Journal of ACM, 28, N. 4:765–768, 1981.CrossRefGoogle Scholar
  17. [PP90]
    F. Parlamento and A. Policriti. Decision procedures for elementary sublanguages of set theory. XIII. Model graphs, reflection and decidability. To appear in J. Automated Reasoning, 1990.Google Scholar
  18. [Pre29]
    M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetic ganzer Zahlen, in welchem die Addition als einsige Operation hervortritt. In Comptes-rendus du Premier Congrès des Mathematiciens des Pays Slaves, pages 192–201,395. Warsaw, 1929.Google Scholar
  19. [Sal75]
    H.M. Salkin. Integer programming. Addison-Wesley Publishing Co., Inc., Reading, Mass., 1975.Google Scholar
  20. [Tar51]
    A. Tarski. A decision method for elementary algebra and geometry. Univ. of California Press, Berkeley, 2nd ed. rev., 1951.Google Scholar
  21. [Tar59]
    A. Tarski. What is elementary geometry? In L. Henkin, P. Suppes, and A. Tarski, editors, The axiomatic method with special reference to geometry and physics, pages 16–29, 1959.Google Scholar
  22. [Wei88]
    V. Weispfenning. The complexity of linear problems in fields. J. Symb. Comp., 5:3–28, 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • D. Cantone
    • 1
  • V. Cutello
    • 2
  • J. T. Schwartz
    • 3
  1. 1.Dipartimento di Matematica Pura e ApplicataUniversità di L'AquilaItaly
  2. 2.International Computer Science InstituteBerkeley
  3. 3.Department of Computer Science Courant Institute of Mathematical SciencesNew York UniversityUSA

Personalised recommendations