ABSTRACT. Not too long ago most headlines talked about our fear of AI. Today, AI is ubiquitous, and the conversation has moved on from whether we should use AI to how we can trust the AI systems that we use in our daily lives. In this talk I look at some key technical ingredients that help us build confidence and trust in using intelligent technology. I argue that intuitiveness, interaction, explainability and inclusion of human domain knowledge are essential in building this trust. I present some of the techniques and methods we are building for making AI systems that think and interact with humans in more intuitive and personalised ways, enabling humans to better understand the solutions produced by machines, and enabling machines to incorporate human domain knowledge in their reasoning and learning processes.

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.

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.

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).

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.

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.

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.

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.