报告人：Xiaohong Chen (University of Illinois at Urbana-Champaign, USA)
地点：Room 1303, Sciences Building No. 1
However, ML and RL has two main limitations. The first limitation is about the existing proof system of ML, which is only applicable to theories that contain a set of special "definedness symbols" with which equality and membership are defined as derived constructs. The second limitation is that ML and RL can only define and reason about reachability properties and is not capable of expressing liveness or many other interesting properties that temporal or dynamic logics can naturally express.
In this talk, I will address the above two limitations. I will present a new proof system of ML that replaces the existing one without requiring the special "definedness symbols", so it can be applied to all theories. Then, I will present a new logic that extends ML with a mu-binder that builds least fixpoints. The resulting logic is called matching mu-logic (MmL), which is proved to subsume not only ML and RL, but many other important logics/calculi in computer science, especially those which are specifically designed to reason about fixpoints and inductive structures and/or properties, including first-order logic with least fixpoints (LFP), modal mu-logic and many temporal logics such as infinite/finite-trace LTL and CTL, and dynamic logic. At the end of the talk, I will discuss some interesting future work about the new ML proof system and the new MmL logic, including ML/MmL's connection to modal logic, the completeness theorems of ML, and the Henkin semantics of MmL.
Bio: Xiaohong Chen (http://fsl.cs.illinois.edu/index.php/Xiaohong_Chen) is a Ph.D. student at University of Illinois at Urbana-Champaign. Before that, he obtained his Bachelor's degree majoring in mathematics at Peking University, China. Xiaohong's main research interest includes formal methods and programming languages, in particular, formal specification and verification and program logics. Xiaohong believes that programming languages and programs should have formal specifications, and verification techniques should be made language-independent.