Some fragments of second-order logic over the reals for which satisfiability and equivalence are (un)decidable

• Autorzy: Grimson R. , Kuijpers B.

Identyfikatory

DOI

10.4467/20842589RM.14.002.2272

• Języki publikacji: EN

Abstrakty

EN

We consider the Σ10 -fragment of second-order logic over the vocabulary [+;x; 0; 1; <; S1; …..., Sk], interpreted over the reals, where the predicate symbols Si are interpreted as semi algebraic sets. We show that, in this context, satisfiability of formulas is decidable for the first-order THERE EXISTS-quantifier fragment and undecidable for the THERE EXISTS*FOR ALL- and FOR ALL*-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.

Słowa kluczowe

EN

second-order logic; equivalence of formulas; containment; (un)decidability results; predicates

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2014
• Tom: Vol. 49
• Strony: 23--34
• Opis fizyczny: Bibliogr. 8 poz.

Twórcy

autor

Grimson R.

• CONICET and Escuela de Ciencia y Tecnologìa, Universidad de San Martìn, Campus Miguelete (CP1650). San Martìn, Provincia de Buenos Aires, Argentina

autor

Kuijpers B.

• Databases and Theoretical Computer Science Group, Hasselt University, Agoralaan, Gebouw D, 3590 Diepenbeek, Belgium

Bibliografia

• [1] J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Volume 36 of Ergebenisse der Mathematik und ihrer Grenzgebiete, Folge 3, Springer-Verlag, Berlin, 1998.
• [2] G. Jeronimo and J. Sabia, On the number of sets definable by polynomials, Journal Algebra 227:2 (2000), 633-644.
• [3] E. Böorger, E. Gräadel and Y. Gurevich, The Classical Decision Problem, Monographs in Mathematical Logic, Springer-Verlag, 2000.
• [4] D. Grigoriev and N. N. (jr.) Vorobjov, Solving systems of polynomial inequalities in subexponential time, Journal of Symbolic Computation 5 (1988), 37-64.
• [5] J. P. Jones and Y. V. Matijasevich, Exponential Diophantine representation of recursively enumerable sets, In J. Stern, editor, Proceedings of the Herbrand Symposium: Logic Colloquium '81, volume 107 of Studies in Logic and the Foundationsof Mathematics, Amsterdam. North Holland, 1982, pp.159-177.
• [6] Y. V. Matijasevich, Hilbert's Tenth Problem, MIT Press, Cambridge, MA, 1993.
• [7] J. Paredaens, G. Kuper and L. Libkin, editors, Constraint databases, Springer-Verlag, 2000.
• [8] A. Tarski, A Decision Method for Elementary Algebra and Geometry, University of California Press, 1951.