AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

30 Minutes

Intuitively, two variables in some logical formula are said to be independent, if there exists a way of equivalently rewriting the formula so that no predicate “connects” both variables. More generally, people study the notion of variable decomposability, which asks whether the given formula can be rewritten as a Boolean combination of predicates each having its free variables within some block of a fixed partition [1, 2, 3]. These definitions capture the intuitive notion of “independence”, whereas the corresponding results and decision procedures have many applications in SMT and string analysis [4], databases [1, 2], automata theory [5] and other areas. Although the variable decomposability problem in general is known to be undecidable [2, Proposition 2], it is decidable for many important first-order theories such as Presburger arithmetic. Not much is known about the computational complexity of variable decomposability problems for many first-order theories – this is an open problem raised in [4]. Apart from this, known techniques allow the construction of efficient decision procedures only for “discrete” first-order theories. My main result is a novel technique for deciding variable independence and variable decomposability efficiently. It works for a large class of “non-discrete” theories, for which known proof techniques do not work. An example of such a theory is linear arithmeticm over Q, for which I improved the known complexity bound. I have discovered a connection between the “convexity” of a logic and the ability to decide variable decomposability efficiently. It turned out that like in mathematical optimization, “the great watershed in optimization isn’t between linearity and nonlinearity, but convexity and nonconvexity”1, a very similar barrier exists in the setting I am working in, that is, deciding variable independence is significantly easier for “convex” first-order theories compared to “non-convex” ones.

Jennifer Gerling

+49 681 9325 1801

--email hidden

Zoom

passcode not visible

logged in users only