Campus Event Calendar
Event Entry
What and Who
The complexity of Presburger arithmetic with power or powers
Dmitry Chistikov
University of Warwick
SWS Colloquium
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 14 November 2023
11:00
60 Minutes
G26
111
Kaiserslautern
Abstract
Presburger arithmetic, or linear integer arithmetic, is known to have decision procedures that work in triply exponential time.
Jointly with M. Benedikt (Oxford) and A. Mansutti (IMDEA Software Institute), we have recently considered two decidable extensions of Presburger arithmetic: with the power function and with the predicate for the set of powers of 2. No elementary decision procedures were known for these two theories.
In this talk, I will introduce this work and outline ideas behind our results. Namely, we have shown that existence of solutions over N to systems of linear equations and constraints of the form $y = 2^x$ can be decided in nondeterministic exponential time. Also, linear integer arithmetic extended with a predicate for powers of 2 can be decided in triply exponential time.
(Based on a paper in ICALP'23.)
Jointly with M. Benedikt (Oxford) and A. Mansutti (IMDEA Software Institute), we have recently considered two decidable extensions of Presburger arithmetic: with the power function and with the predicate for the set of powers of 2. No elementary decision procedures were known for these two theories.
In this talk, I will introduce this work and outline ideas behind our results. Namely, we have shown that existence of solutions over N to systems of linear equations and constraints of the form $y = 2^x$ can be decided in nondeterministic exponential time. Also, linear integer arithmetic extended with a predicate for powers of 2 can be decided in triply exponential time.
(Based on a paper in ICALP'23.)
Contact
Susanne Girard
+49 631 9303 9605
--email hidden
passcode not visible
logged in users only
Susanne Girard, 11/09/2023 13:30 -- Created document.