View: session overviewtalk overview

10:30 | Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness PRESENTER: Guilherme Toledo ABSTRACT. We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the Boolean combinations of the most common model-theoretic properties in theory combination, namely stable-infiniteness, smoothness, convexity, finite witnessability and strong finite witnessability (and therefore politeness and strong politeness as well); all of our examples are sharp, in the sense that we also offer proofs that no theories are available within simpler signatures. This table profoundly progresses the current understanding of the various properties and their interactions. The most remarkable example in this table is of a theory that is polite but not strongly polite, over a single sort (the existence of such a theory was only known until now for two-sorted signatures). The second contribution is a new combination theorem, according to which polite theory combination can be done for theories that are stably-infinite and strongly finitely witnessable, thus showing that smoothness is not a critical property in this combination method. This result has the potential of greatly simplifying proofs that show that a certain theory can be combined with any other theory using polite combination, as proving stable-infiniteness is much simpler than proving smoothness. |

11:00 | PRESENTER: Elisabeth Henkel ABSTRACT. We present a generic tree-interpolation algorithm in the SMT context with quantifiers. The algorithm takes a proof of unsatisfiability using resolution and quantifier instantiation and computes interpolants (which may contain quantifiers). Arbitrary SMT theories are supported, as long as each theory itself supports tree interpolation for its lemmas. In particular, we show this for the theory combination of equality with uninterpreted functions and linear arithmetic. The interpolants can be tweaked by virtually assigning each literal in the proof to interpolation partitions (colouring the literals) in arbitrary ways. The algorithm is implemented in SMTInterpol. |

11:30 | PRESENTER: Stéphane Graham-Lengrand ABSTRACT. This paper presents and proves totally correct a new algorithm, called QSMA, for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of QSMA implemented in YicesQS is described and shown to preserve total correctness. A report on the performance of YicesQS at the 2022 SMT competition is included. YicesQS ran in the LIA, NIA, LRA, NRA, and BV categories and ranked second for the “largest contribution” award (single queries). It was the only solver to solve all LRA instances, where it was about 2 orders of magnitude faster than the second best solver (Z3). |

12:00 | PRESENTER: Nikolaj Bjorner ABSTRACT. We introduce a calculus for incremental pre-processing for SMT and instantiate it in the context of z3. It identifies when powerful formula simplifications can be retained when adding new constraints. Use cases that could not be solved in incremental mode can now be solved incrementally thanks to the availability of pre-processing. Our approach admits a class of transformations that preserve satisfiability, but not equivalence. We establish a taxonomy of pre-processing techniques that distinguishes cases where new constraints are modified or constraints previously added have to be replayed. We then justify the soundness of the proposed incremental pre-processing calculus. |

14:00 | Decidability of difference logic over the reals with uninterpreted unary predicates PRESENTER: Baptiste Vergain ABSTRACT. 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. |

14:30 | On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$ PRESENTER: Viorica Sofronie-Stokkermans ABSTRACT. We study the $P$-interpolation property for certain local theory extensions, and use the results we establish for proving $\leq$-interpolation in classes of semilattices with monotone operators. For computing the $\leq$-interpolating terms, we use a hierarchic approach. We use these results for the study of interpolation in ${\cal EL}$ and ${\cal EL}^+$, and present an implementation. |

15:00 | PRESENTER: Marvin Brieger ABSTRACT. This paper introduces a uniform substitution calculus for dL_CHP, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when generalized to dL_CHP manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for dL_CHP paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism. |