[logic-ml] Norbert Müller's Talk, Tue 15 Oct, Fukuoka

[Akitoshi Kawamura]

皆様

九州大学の河村と申します。ノルベルト・ミュラー先生（トリール大）の講演を
下記の通り来週火曜日に九大で開催いたします。宜しければぜひお越し下さい。
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.
----------------------------------------------------------------------

-- 
河村彰星
九州大学システム情報科学研究院情報学部門
〒819-0395　福岡市西区元岡744
092-802-3806
kawamura at inf.kyushu-u.ac.jp