[The logic of fractional parts of real numbers]
The group of decimals with addition modulo 1 and the natural order, which is not an ordered group in the usual sense, is used to enhance the efficiency of timed automata of Bouchy, Finkel and Leroux (Decomposition of decidable first-order logics over integers and reals, in: Temporal Representation and Reasoning, Proceedings of the 15th Symposium TIME 2008, IEEE Computer Society Press, 2008, pp. 147–155). In this note, we axiomatize this structure and show that it admits quantifier elimination.
Le groupe des décimales avec l'addition modulo 1 et l'ordre naturel, qui n'est pas un groupe ordonné au sens habituel, est utilisé pour améliorer l'efficacité des automates temporels de Bouchy, Finkel et Leroux (Decomposition of decidable first-order logics over integers and reals, in : Temporal Representation and Reasoning, Proceedings of the 15th Symposium TIME 2008, IEEE Computer Society Press, 2008, pp. 147–155). Dans cette note, on donne une axiomatisation de cette structure, et on montre qu'elle admet l'élimination des quantificateurs.
Accepted:
Published online:
Luc Bélair 1; Françoise Point 2
@article{CRMATH_2016__354_7_645_0, author = {Luc B\'elair and Fran\c{c}oise Point}, title = {La logique des parties fractionnaires de nombres r\'eels}, journal = {Comptes Rendus. Math\'ematique}, pages = {645--648}, publisher = {Elsevier}, volume = {354}, number = {7}, year = {2016}, doi = {10.1016/j.crma.2016.04.009}, language = {fr}, }
Luc Bélair; Françoise Point. La logique des parties fractionnaires de nombres réels. Comptes Rendus. Mathématique, Volume 354 (2016) no. 7, pp. 645-648. doi : 10.1016/j.crma.2016.04.009. https://comptes-rendus.academie-sciences.fr/mathematique/articles/10.1016/j.crma.2016.04.009/
[1] Decomposition of decidable first-order logics over integers and reals, Temporal Representation and Reasoning, Proceedings of the 15th Symposium TIME 2008, IEEE Computer Society Press, 2008, pp. 147-155
[2] Totally ordered commutative semigroups, Bull. Amer. Math. Soc., Volume 64 (1958), pp. 305-316
[3] M. Giraudet, G. Leloup, F. Lucas, First-order theory of cyclically ordered groups, 2013, arXiv:13-11.0499.
[4] Quantifier elimination for lexicographic products of ordered Abelian groups, Tsukuba J. Math., Volume 33 (2009), pp. 95-129
[5] Autour des groupes cycliquement ordonnés, Ann. Fac. Sci. Toulouse – Math., Volume XXI (2012), pp. 235-257
[6] Théorie des modèles des groupes cycliquement ordonnés divisibles, Séminaire de structures algébriques ordonnés, vol. 56, Prépublications de l'université Paris-7, 1996
[7] Mixed real-integer linear quantifier elimination, Symbolic and Algebraic Computation, Proceedings ISSAC'99, ACM, Vancouver, BC, 1999, pp. 129-136
Cited by Sources:
Comments - Policy