(11 month) 20th November 2025
WHO: Dr. Yoni Zohar, Bar-Ilan University
WHEN: Thursday, November 20th , 2025 at 12:00
WHERE: BUILDING 503 (Computer Science) AUDITORIUM
Title: My Attempts To Save Politeness
Abstract:
Theory combination in Satisfiability Modulo Theories (SMT) deals with combining algorithms for proving formulas over integers, bit-vectors, data structures, and more.
Among the most important combination methods is the polite combination method, which only requires that one of the theories admits some property, while the other theory can be any decidable theory.
When polite combination was introduced, it was claimed that the required property is "politeness", a notion I will formally and intuitively describe in my talk. But later, it was shown that the correctness proof had a bug, and for the proof to work, a stronger property is needed, namely "strong politeness".
This led to the following question: can politeness still be useful for theory combination?
In this talk I will describe several attempts made by myself and others to answer this question positively, thus saving the politeness property.
No background in theory combination or SMT is assumed, though politeness is expected.
