Comptes Rendus
no. 7
Logique
La logique des parties fractionnaires de nombres réels

Présenté par : le comité de rédaction

Luc Bélair1 ; Françoise Point2
1 Département de mathématiques, université du Québec, C.P. 8888, succ. Centre-ville, Montréal, Québec, H3C 3P8, Canada
2 Département de mathématiques, université de Mons, Le Pentagone, 20, place du Parc, B-7000 Mons, Belgique
Comptes Rendus. Mathématique, Volume 354 (2016) no. 7, pp. 645-648.

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.

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.

Reçu le :
Accepté le :
Publié le :
DOI : 10.1016/j.crma.2016.04.009
Luc Bélair 1 ; Françoise Point 2

1 Département de mathématiques, université du Québec, C.P. 8888, succ. Centre-ville, Montréal, Québec, H3C 3P8, Canada
2 Département de mathématiques, université de Mons, Le Pentagone, 20, place du Parc, B-7000 Mons, Belgique 
@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},
}
TY  - JOUR
AU  - Luc Bélair
AU  - Françoise Point
TI  - La logique des parties fractionnaires de nombres réels
JO  - Comptes Rendus. Mathématique
PY  - 2016
SP  - 645
EP  - 648
VL  - 354
IS  - 7
PB  - Elsevier
DO  - 10.1016/j.crma.2016.04.009
LA  - fr
ID  - CRMATH_2016__354_7_645_0
ER  - 
%0 Journal Article
%A Luc Bélair
%A Françoise Point
%T La logique des parties fractionnaires de nombres réels
%J Comptes Rendus. Mathématique
%D 2016
%P 645-648
%V 354
%N 7
%I Elsevier
%R 10.1016/j.crma.2016.04.009
%G fr
%F CRMATH_2016__354_7_645_0
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] F. Bouchy; A. Finkel; J. Leroux 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] A. Clifford 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] S. Ibuka; H. Kikyo; H. Tanaka Quantifier elimination for lexicographic products of ordered Abelian groups, Tsukuba J. Math., Volume 33 (2009), pp. 95-129

[5] G. Leloup Autour des groupes cycliquement ordonnés, Ann. Fac. Sci. Toulouse – Math., Volume XXI (2012), pp. 235-257

[6] F. Lucas 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] W. Weispfenning Mixed real-integer linear quantifier elimination, Symbolic and Algebraic Computation, Proceedings ISSAC'99, ACM, Vancouver, BC, 1999, pp. 129-136

Cité par Sources :

Commentaires - Politique

Ces articles pourraient vous intéresser

Élimination des quantificateurs dans les équations aux différences linéaires sur les vecteurs de Witt

Luc Bélair; Françoise Point

C. R. Math (2008)

Ensembles définissables dans les corps ordonnés différentiellement clos

Françoise Point

C. R. Math (2011)

Une axiomatisation de la substitution

Marcel Crabbé

C. R. Math (2004)