Decidability of difference logic over the reals with uninterpreted unary predicates. (English) Zbl 07838507
Pientka, Brigitte (ed.) et al., Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14132, 542-559 (2023).
Summary: First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single uninterpreted unary predicate. In the SMT world, difference logic is a quite popular fragment of linear arithmetic which is less expressive than Presburger arithmetic. Difference logic on integers with uninterpreted unary predicates is known to be decidable, even in the presence of quantifiers. We here show that (quantified) difference logic on real numbers with a single uninterpreted unary predicate is undecidable, quite surprisingly. Moreover, we prove that difference logic on integers, together with order on reals, combined with uninterpreted unary predicates, remains decidable.
For the entire collection see [Zbl 1535.68012].
For the entire collection see [Zbl 1535.68012].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Boigelot, B., Fontaine, P., Vergain, B.: Decidability of difference logics with unary predicates. In: Proceedings, 7th International Workshop on Satisfiability Checking and Symbolic Computation (2022) |
| [2] | Boigelot, B., Fontaine, P., Vergain, B.: Decidability of difference logic over the reals with uninterpreted unary predicates. arXiv preprint arXiv:2305.15059 (2023) |
| [3] | Bruyère, V.; Carton, O., Automata on linear orderings, J. Comput. Syst. Sci., 73, 1, 1-24 (2007) · Zbl 1178.68307 · doi:10.1016/j.jcss.2006.10.009 |
| [4] | Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science (1962) · Zbl 0147.25103 |
| [5] | Burgess, JP; Gurevich, Y., The decision problem for linear temporal logic, Notre Dame J. Formal Logic, 26, 2, 115-128 (1985) · Zbl 0573.03004 · doi:10.1305/ndjfl/1093870820 |
| [6] | Cristau, J.: Automata and temporal logic over arbitrary linear time. In: FSTTCS 2009. LIPIcs, vol. 4, pp. 133-144 (2009) · Zbl 1248.68293 |
| [7] | Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Center for Research in Computer Technology, Harvard University, Technical report (1972) |
| [8] | Enderton, HB, A Mathematical Introduction to Logic (2001), Boston: Academic Press, Boston · Zbl 0992.03001 |
| [9] | Gurevich, Y.; Shelah, S., Monadic theory of order and topology in ZFC, Ann. Math. Logic, 23, 2-3, 179-198 (1982) · Zbl 0516.03007 · doi:10.1016/0003-4843(82)90004-3 |
| [10] | Haase, C., A survival guide to Presburger arithmetic, ACM SIGLOG News, 5, 3, 67-82 (2018) · doi:10.1145/3242953.3242964 |
| [11] | Halpern, JY, Presburger arithmetic with unary predicates is \(\Pi_1^1\) complete, J. Symbolic Logic, 56, 2, 637-642 (1991) · Zbl 0738.03017 · doi:10.2307/2274706 |
| [12] | Matiyasevich, YV, Hilbert’s Tenth Problem (1993), Cambridge: MIT Press, Cambridge · Zbl 0790.03009 |
| [13] | Rabinovich, A., Temporal logics over linear time domains are in PSPACE, Inf. Comput., 210, 40-67 (2012) · Zbl 1280.68112 · doi:10.1016/j.ic.2011.11.002 |
| [14] | Reynolds, M., The complexity of temporal logic over the reals, Ann. Pure Appl. Logic, 161, 8, 1063-1096 (2010) · Zbl 1235.03052 · doi:10.1016/j.apal.2010.01.002 |
| [15] | Rosenstein, JG, Linear Orderings (1982), Cambridge: Academic Press, Cambridge · Zbl 0488.04002 |
| [16] | Shannon, CE, A universal Turing machine with two internal states, Automata Stud., 34, 157-165 (1956) |
| [17] | Shelah, S., The monadic theory of order, Ann. Math., 102, 3, 379-419 (1975) · Zbl 0345.02034 · doi:10.2307/1971037 |
| [18] | Sierpiński, W., Cardinal and ordinal numbers (1965), Warszawa: PWN, Warszawa · Zbl 0131.24801 |
| [19] | Speranski, SO, A note on definability in fragments of arithmetic with free unary predicates, Arch. Math. Log., 52, 5-6, 507-516 (2013) · Zbl 1279.03066 · doi:10.1007/s00153-013-0328-9 |
| [20] | Tarski, A., A Decision Method for Elementary Algebra and Geometry (1951), Berkeley: University of California Press, Berkeley · Zbl 0044.25102 · doi:10.1525/9780520348097 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
