Despite decades of research, reasoning efficiently about formulas containing both quantifiers and built-in symbols for a given background theory remains a challenge in automated deduction. Nevertheless, several exciting advances have been made in the last few years, mainly in two directions: (i) integrating theory reasoning in saturation-based calculi for first-order logic and (ii) integrating quantified reasoning into frameworks for ground Satisfiability Modulo Theories (SMT). Focusing on the latter, this talk provides an overview of a general, refutation-based approach for reasoning about quantified formulas in SMT. The approach maintains a set S of ground formulas that is incrementally expanded with selected instances of quantified input formulas, with the selection based on counter-models of S. In addition to being quite effective in practice, for several logical theories that admit quantifier elimination and have a decidable universal fragment this approach also leads to practically efficient decision procedures for the full theory. While the approach applies to traditional theories with quantifier elimination such as linear real and integer arithmetic, this talk will present new promising developments for the theory of fixed-sized bit vectors and the theory of floating point arithmetic whose full-fragments are notoriously difficult to reason about.
展开▼
