皆様

九州大学の河村と申します。ノルベルト・ミュラー先生（トリール大）の講演を 下記の通り来週火曜日に九大で開催いたします。宜しければぜひお越し下さい。 http://www.fc.inf.kyushu-u.ac.jp/seminars/R011015.html

---------------------------------------------------------------------- October 15, 2019, Tuesday, 15:00– Room 1019, Ito Campus West Building 2, Kyushu University (九州大学伊都キャンパスウエスト二号館1019室) ---------------------------------------------------------------------- Joint approximations for multivariate real functions Norbert Müller (Universität Trier) ----------------------------------------------------------------------

As a generalization of the well-known NP-complete problem SAT from propositional logic, the task in SMT (Satisfiability Modulo Theories) is to determine whether certain quantifier-free formulae in first-order logic are satisfiable. Popular solvers for such problems are Z3, CVC4 or MathSAT.

We are interested in the case where the first-order logic is on real numbers. For formulae describing linear arithmetic on this set, the implementations mentioned above are quite efficient (as far as possible, having to deal with NP-completeness).

However, nonlinear arithmetic on real numbers is far harder, as general issues concerning decidability arise. In addition, techniques for the treatment of nonlinear formulae are still under development. Our approach combines ideas from CDCL-style SMT solving, computable analysis and the numerical approach of Taylor models.

In the talk we will give brief introductions into these topics and present a prototypical implementation meant for augmenting existing SMT solvers with nonlinear arithmetic. ----------------------------------------------------------------------