On the Theory of Order Over Real Numbers

First-order logic; Real numbers; Satisfiability; Theory of order; Computational Mathematics; Computational Theory and Mathematics; Applied Mathematics

Abstract :

[en] We consider the first-order theory of order over real numbers extended with monadic uninterpreted predicates. It has long been established that this theory is decidable, by different approaches such as a reduction to linear-time temporal logic over the reals, expressing the problem as a particular case of deciding the first-order theory of all linear orderings, or reasoning about restrictions of the monadic second-order theory of order. The main contribution of this work is to provide a complete self-contained proof of decidability for this logic. Additionally, our proof develops a symbolic notation system for models of satisfiable formulas, which can be seen as a first step towards an actual implementation of a decision procedure for the theory of order over the reals.

Research Center/Unit :

Montefiore Institute - Montefiore Institute of Electrical Engineering and Computer Science - ULiège

Disciplines :

Computer science

Author, co-author :

Boigelot, Bernard ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Informatique

Fontaine, Pascal ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Systèmes informatiques distribués

Vergain, Baptiste ; Université de Liège - ULiège > Montefiore Institute of Electrical Engineering and Computer Science

Language :

English

Title :

On the Theory of Order Over Real Numbers

Publication date :

03 April 2026

Journal title :

Mathematics in Computer Science

ISSN :

1661-8270

eISSN :

1661-8289

Publisher :

Birkhauser

Volume :

Issue :

Peer reviewed :

Peer reviewed

Additional URL :

https://link.springer.com/content/pdf/10.1007/s11786-025-00624-2.pdf

Funding text :

This research was partially supported in part by an Amazon Research Award, Fall 2022 CFP. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not reflect the views of Amazon. This work was also partially supported by the Fonds de la Recherche Scientifique - FNRS WEAVE under Grant number T.W028.23.

Available on ORBi :

since 24 August 2026

Statistics

Number of views

46 (3 by ULiège)

Number of downloads

15 (1 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenAlex citations

Bibliography

Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of International Congress on Logic, Methodology and Philosophy of Science, pp. 1–12 (1962)
Büchi JR The Monadic Second-order Theory of All Countable Ordinals. Decidable theories 1973 Berlin Springer 2
Gurevich Y Magidor M Shelah S The monadic theory of ω2 J. Symbol. Logic 1983 48 2 387 398 10.2307/2273556
Ehrenfeucht A Decidability of the theory of linear ordering relation Not. Am. Math. Soc. 1959 6 3 268 269
Läuchli H Leonard J On the elementary theory of linear order Fundam. Math. 1966 59 1 109 116 199108 10.4064/fm-59-1-109-116
Fraïssé R Sur l’extension aux relations de quelques propriétés des ordres Ann. Sci. de l’École Normale Supérieure 1954 71 4 363 388 69239 10.24033/asens.1027
Ehrenfeucht A An application of games to the completeness problem for formalized theories Fundam. Math. 1961 49 2 129 141 126370 10.4064/fm-49-2-129-141
Läuchli, H.: A decision procedure for the weak second-order theory of linear order. In: Contributions to Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol. 50, pp. 189–197. Elsevier, Amsterdam (1968)
Shelah S The monadic theory of order Ann. Math. 1975 102 3 379 419 491120 10.2307/1971037
Thomas, W.: Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In: Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht. Lecture Notes in Computer Science, pp. 118–143 (1997)
Rabin MO Decidability of second-order theories and automata on infinite trees Trans. Am. Math. Soc. 1969 141 1 35 246760
Kamp, H.: Tense logic and the theory of linear order. Ph.D. thesis, University of California at Los Angeles (1968)
Rabinovich, A.: A proof of Kamp’s theorem. Logical Methods in Computer Science 10(1) (2014)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of 7th ACM Symposium on Principles of Programming Languages (POPL), pp. 163–170. ACM Press, New-York (1980)
Burgess JP Gurevich Y The decision problem for linear temporal logic Notre Dame J. Form. Logic 1985 26 115 128 783592
Reynolds M The complexity of the temporal logic with “until” over general linear time J. Comput. Syst. Sci. 2003 66 2 393 426 1976021 10.1016/S0022-0000(03)00005-9
Reynolds M The complexity of decision problems for linear temporal logics J. Stud. Log 2010 3 1 19 50 566553
Reynolds M The complexity of temporal logic over the reals Ann. Pure Appl. Logic 2010 161 8 1063 1096 2629506 10.1016/j.apal.2010.01.002
Rabinovich, A.: Temporal logics over linear time domains are in PSPACE. Inf. Comput. 210, 40–67 (2012)
Barrett, C., Kroening, D., Melham, T.: Problem solving for the 21st century: Efficient solvers for satisfiability modulo theories. Technical Report 3, London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering (2014)
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009). Chap. 26
Habermehl, P., Hecko, M., Havlena, V., Holík, L., Lengál, O.: Algebraic reasoning meets automata in solving linear integer arithmetic. In: Proc. Intl. Conf. on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 14681, pp. 42–67. Springer, Berlin, Heidelberg (2024)
Ebbinghaus H-D Flum J Finite Model Theory 1995 Berlin Springer 10.1007/978-3-662-03182-7
Ramsey FP On a problem of formal logic Proc. Lond. Math. Soc. 1930 30 264 286 1576401 10.1112/plms/s2-30.1.264
Bruyère V Carton O Automata on linear orderings J. Comput. Syst. Sci. 2007 73 1 1 24 2279028 10.1016/j.jcss.2006.10.009
Boigelot, B., Fontaine, P., Vergain, B.: Non-emptiness test for automata over words indexed by the reals and rationals. In: Fazekas, S.Z. (ed.) Proceedings of International Conference on Implementation and Application of Automata (CIAA). Lecture Notes in Computer Science, vol. 15015, pp. 94–108. Springer, Cham (2024)
Boigelot, B., Fontaine, P., Vergain, B.: Universal first-order quantification over automata. In: Nagy, B. (ed.) Proceedings of International Conference on Implementation and Application of Automata (CIAA). Lecture Notes in Computer Science, vol. 14151, pp. 91–102. Springer, Cham (2023)