nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

\(\langle \mathbb {R}, +,<,1 \rangle \) Is Decidable in \(\langle \mathbb {R}, +,< ,\mathbb {Z}\rangle \)

verfasst von : Alexis Bès, Christian Choffrut

Erschienen in: Language and Automata Theory and Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We show that it is decidable whether or not a relation on the reals definable in the structure \(\langle \mathbb {R}, +,< ,\mathbb {Z}\rangle \) can be defined in the structure \(\langle \mathbb {R}, +,<,1 \rangle \). This result is achieved by obtaining a topological characterization of \(\langle \mathbb {R}, +,<,1 \rangle \)-definable relations in the family of \(\langle \mathbb {R}, +,< ,\mathbb {Z}\rangle \)-definable relations and then by following Muchnik’s approach of showing that this characterization can be expressed in the logic of \(\langle \mathbb {R}, +,<,1 \rangle \).

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Nonstandard Cayley Automatic Representations for Fundamental Groups of Torus Bundles over the Circle

Nächstes Kapitel Ordered Semiautomatic Rings with Applications to Geometry

Becker, B., Dax, C., Eisinger, J., Klaedtke, F.: LIRA: handling constraints of linear arithmetics over the integers and the reals. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 307–310. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_36CrossRef

Bieri, H., Nef, W.: Elementary set operations with d-dimensional polyhedra. In: Noltemeier, H. (ed.) CG 1988. LNCS, vol. 333, pp. 97–112. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-50335-8_28CrossRef

Boigelot, B., Brusten, J., Bruyère., V.: On the sets of real numbers recognized by finite automata in multiple bases. LMCS 6(1), 1–17 (2010)

Boigelot, B.: The Liege automata-based symbolic handler (LASH). http://www.montefiore.ulg.ac.be/ boigelot/research/lash/

Boigelot, B., Brusten, J.: A generalization of Cobham’s theorem to automata over real numbers. Theor. Comput. Sci. 410(18), 1694–1703 (2009)MathSciNetCrossRef

Boigelot, B., Brusten, J., Leroux, J.: A generalization of Semenov’s theorem to automata over real numbers. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 469–484. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_34CrossRef

Boigelot, B., Rassart, S., Wolper, P.: On the expressiveness of real and integer arithmetic automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 152–163. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055049CrossRefMATH

Bouchy, F., Finkel, A., Leroux, J.: Decomposition of decidable first-order logics over integers and reals. In: 2008 15th International Symposium on Temporal Representation and Reasoning, pp. 147–155. IEEE (2008)

Büchi, J.R.: On a decision method in the restricted second-order arithmetic. In: Proceedings International Congress Logic, Methodology and Philosophy of Science, Berkeley 1960, pp. 1–11. Stanford University Press (1962)

10.

Choffrut, C., Frigeri, A.: Deciding whether the ordering is necessary in a Presburger formula. DMTCS 12(1), 20–38 (2010)MathSciNetMATH

11.

Cobham, A.: On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theor. 3(2), 186–192 (1969)MathSciNetCrossRef

12.

Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69–76 (1975)MathSciNetCrossRef

13.

Fränzle, M., Quaas, K., Shirmohammadi, M., Worrell, J.: Effective definability of the reachability relation in timed automata. Inf. Proc. Lett. 153, 105871 (2020)

14.

Leroux, J.: A polynomial time Presburger criterion and synthesis for number decision diagrams. In: Proceedings of LICS 2005, pp. 147–156. IEEE (2005)

15.

Milchior, A.: Büchi automata recognizing sets of reals definable in first-order logic with addition and order. In: Gopal, T.V., Jäger, G., Steila, S. (eds.) TAMC 2017. LNCS, vol. 10185, pp. 440–454. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-55911-7_32CrossRefMATH

16.

Miller, C.: Expansions of dense linear orders with the intermediate value property. J. Symb. Logic 66(4), 1783–1790 (2001)MathSciNetCrossRef

17.

Muchnik, A.A.: The definable criterion for definability in Presburger arithmetic and its applications. Theor. Comput. Sci. 290(3), 1433–1444 (2003)MathSciNetCrossRef

18.

Presburger, M.: Uber die vollstandigkeit eines gewissen systems der arithmetic ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: du Premier Congrès des Mathématiciens des Pays Slaves, Warsaw, vol. 395, pp. 92–101 (1927)

19.

Semenov, A.L.: Presburgerness of predicates regular in two number systems. Siberian Math. J. 18(2), 289–300 (1977)CrossRef

20.

Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC 1999, pp. 129–136. ACM, New York (1999)

Titel: Is Decidable in
verfasst von: Alexis Bès
Christian Choffrut
Verlag: Springer International Publishing
Buch: Language and Automata Theory and Applications
Print ISBN: 978-3-030-40607-3

Electronic ISBN: 978-3-030-40608-0

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-40608-0_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"