Reasoning About Hilbert’s Choice Operator in SMT
summary
Proposes adding Hilbert ε-terms to SMT by translating quantifiers to choice terms, then replacing those with fresh logical constants (e.g. introduce L1 and L2) and treating the ε-axioms as a small, syntactic family of refinements; unsat is found by choosing terms T for those axioms (the algorithm searches over T instantiations) and solving a quantifier-free SMT model (CVC5/Amazon trusted solver used), so the SMT core never needs quantifier reasoning. Implementation is currently sequential but explicitly designed to scale via distributed portfolios and shared refinements.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:49Motivation for distributed SMT solving
- 11:02Hilbert’s epsilon calculus and quantifiers
- 17:25Sequential algorithm example
- 20:13Epsilon-based approach advantages
- 23:47Tribute to Andreas Podelski
- 24:52Q&A: Distributed solving limits
- 27:03Q&A: Distributed verification
- 28:30Q&A: Technique applicability
- 30:12Q&A: Comparison with other methods
related talks
35mThe Mastermind behind Refinement Types
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
19mSMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
27mSM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
13mProgram Analysis via Efficient Symbolic Abstraction
59mUnification Modulo Equational Theories in Languages with Binding Operators
29mExplicit Refinement Types