Time: 10:45-12:00, Monday, April 23, 2018

Venue: Room 201, Caoguangbiao Main Building, Yuquan Campus

Speaker: Professor James Davenport, University of Bath, UK

James Davenport is Hebron & Medlock Professor of Information Technology at the University of Bath. He is an author of textbook “Computer Algebra: Systems and Algorithms for Algebraic Computation”. His research interests include computer algebra, especially symbolic integration and simplification, equation solving, electronic mathematical publishing and "mathematics on the (semantic) Web", robot motion planning and cryptography, especially cracking US public-key cryptosystems. He has also published in complexity theory, type theory and in networking. Outside interests include examining French PhDs.

Abstract:

The EU Symbolic Computation and Satisfiability Checking � SC² network (http://www.sc-square.org/CSA) looks at the interaction between Satisfiability Checking (notably Satisfiability Modulo Theories � SMT) and Symbolic Computation (Computer Algebra). In theory, both can consider problems such as (f1 = 0 ^ g1 > 0) V (f2 = 0 ^ g2 < 0) for polynomial fi ; gj. But the two approach these problems in different ways: Satisfiability Checking looks at the logic first, and Symbolic Computation the geometry of the polynomials first. We will sketch the two points of view, and talk about some recent progress in taking a more holistic view of the problem.