<cite id="xvznh"><span id="xvznh"><var id="xvznh"></var></span></cite>
<span id="xvznh"><video id="xvznh"></video></span><strike id="xvznh"><dl id="xvznh"></dl></strike>
<th id="xvznh"><noframes id="xvznh"><span id="xvznh"></span>
<strike id="xvznh"></strike><span id="xvznh"></span>
<ruby id="xvznh"></ruby>
<strike id="xvznh"></strike>
<strike id="xvznh"><dl id="xvznh"></dl></strike><strike id="xvznh"><i id="xvznh"></i></strike>
<span id="xvznh"></span>
12月6日:Pierre-Louis Curien
發布時間:2019-11-28  閱讀次數:8351

報告題目:Proofs and surfaces

報告人:Pierre-Louis Curien. (魯思教授)

報告人單位:Emeritus senior CNRS researcher (IRIF, Université Paris Diderot, CNRS, and Inria)

時間:2019年12月06日10:00-11:30

地點:數學館201
主持人:鄧玉欣教授

 

報告摘要:

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.  

 

報告人簡介:

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.  

華東師范大學軟件工程學院
www.pusatkosmetika.com Copyright Software Engineering Institute
院長信箱:yuanzhang@sei.ecnu.edu.cn | 院辦電話:021-62232550 | 學院地址:上海中山北路3663號理科大樓
999彩票app下载软件