讲座题目：Proofs and surfaces 主讲人：Pierre-Louis Curien 主持人：邓玉欣 教授 开始时间：2019-12-6 10:00:00 讲座地址：数学馆201 主办单位：软件工程学院
报告人简介： Pierre-Louis Curien is Emeritus senior CNRS researcher at IRIF Laboratory (University Paris 7 and CNRS).He graduated from Ecole normale Supérieure (Paris), and received his PhD and « Thèse d’Etat » from University Paris 7 in 1979 and 1983, respectively. He received the IBM France prize in 1990. His research interests spread over computer science and mathematics, and cover the semantics of programming languages, category theory, ane more recently homotopical algebra. He was director or deputy-director of various research structures in France. He created the Inria joint team pi.r2 (whose research is build around the proof assistant Coq) in 2009 and headed it until his retirement in October 2019.
报告内容： Incidence theorems in Euclidean or projective geometry state that some incidences follow from other incidences, where a preincidence is a pair of a line and a point (or three points), and an incidence is a preincidence together with the information whether the point lies on the line or not.As remarked by Richter-Gebert, oriented closed surfaces given by triangular complexes give rise to such incidence results, in the form that preincidences are attached to each triangle (they are called a Menelaus situation), and whenever all but one of these Menelaus situations hold (i.e.the preincidences are incidences), then so do the ones of the triangle left out.This gives rise to a logical system based on unilateral sequents with the intended meaning that each formula is implied by the remaining ones. It also gives rise to a cyclic operad (the notion will be explained in the talk),of which we give a presentation by generators and relations. |
