Decision Problems in Geometry and Analysis

Rob Arthan

(Lemma 1 Ltd/Queen Mary)

Powerful automatic proof procedures are essential for the application of formal methods in engineering and for the solution of verification problems in mathematics. I will describe some recent work on the decision problems for the natural two-sorted first-order theories for metric spaces, Hilbert spaces and Banach spaces. It turns out that the theory of Hilbert spaces is decidable via a reduction to the first-order theory of the reals while the theories of metric spaces and Banach spaces are undecidable in a very strong sense. The undecidability stems from phenomena that begin in dimension two and the proofs are quite pictorial. Despite the undecidability results, there are decision procedures that have proved useful in practice for fragments of the theory of Banach spaces. I will report on these and on a little challenge problem for automated proof in the real trigonometric field arising from the work on undecidability.
Thursday 3rd December 2009, 14:00
Far-134 (Video conferencing room)
Department of Computer Science