时间：3月26日  上午9:00  
　　地点：京师学堂三楼第七会议厅

　　议程：

9:00-9:45
报告一
报告人: 王捍贫 北京大学
题   目: 一种云存储系统的建模与验证
摘   要: 云计算作为一种新的计算范型，有可能成为下一代计算的主流模式。云存储是云计算的基础（infostructure)，其基本的存储单元是块(block, chunk)。目前人们主要讨论基于云存储系统的大数据信息的利用问题，而对这种分布式、多副本的存储方式的可靠性与管理正确性问题研究不够。本讲座介绍一种基于分离逻辑的云存储管理系统的建模与验证方法。在云存储系统中，不仅有传统的存储地址，还有块地址和文件变量，使得描述云存储管理系统的逻辑变得复杂，大量问题尚待进一步研究。

9:45-10:00　茶歇

10:00-10:45　　

报告二
报告人: 郭美云 西南大学
题   目: 试析根岑逻辑演绎思想的主要特征和哲学影响
摘   要: 根岑是自然演绎和矢列演算的创立者。在根岑的两个演绎系统中，每个逻辑符号都由引入和消去一对规则组成。根岑认为，引入规则定义了逻辑符号的意义，而消去规则只是引入规则的后果。根岑的上述思想加上他采取的树形证明方式引导他发现并证明了切割消去定理，即每个推演都可以归约为一种正规的证明形式。这种正规的证明形式没有弯路并具有子公式性质，从而可以将其应用到不可演绎的证明和算术系统的一致性证明中去。根岑关于逻辑符号的意义思想对语言哲学中的意义理论和证明论语义学的提出都产生了深远影响。

10:45-11:00　茶歇

11:00-11:45
报告三
报告人: 宋诗畅 北京交通大学
题   目: On the automorphism group of Hall's universal locally finite group
摘   要: It is well-known that Hall's universal locally finite group H is the Fraisse limit of the class of finite groups. In this talk, we follow Kechris and Rosendal's work to study topological properties of conjugacy classes in the automorphism group Aut(H) of Hall's universal locally finite group. Specifically, we show that Aut(H) has ample generics, and thus it has small index property and it is automatically continuous.

11:45-14:00　午餐

14:00-14:45
报告四
报告人: 尹志 安徽工程大学
题   目: Borel reducibility between equivalence relations generated by sequence spaces
摘   要: Borel reduction is a fundamental concept in descriptive set theory, we often use it to compare the complexity of dierent equivalence relations. In recent years, many equivalence relations concerning Banach space theory were investigated. In this talk, we will discuss the complexity of several equivalence relations generated by sequence spaces under Borel reduction. We will report the recent developments of Borel reducibility between the landmark equivalence relations and equivalence relations generated by these spaces, and mutual Borel reducibility between these equivalence relations. Some of the results are joint work with Longyun Ding and Su Gao.

14:45-15:00　　茶歇

15:00-15:45
报告五
报告人: 俞珺华 清华大学
题   目: Self-referentiality in provability semantics of intuitionistic logic
摘   要: This talk is about works on the topic of self-referentiality in provability semantics of intuitionistic logic formalized in the Goedel--Artemov approach. This approach consists of three steps: (1) intuitionistic propositional calculus (IPC) is embedded in modal logic S4; (2) S4 has the Logic of Proofs (LP) as its explicit version; and (3) LP is interpreted in Peano Arithmetic. In another word, LP serves as a gateway via which S4 and hence IPC get their provability semantics. In LP, there are legal formulas of the form "t : phi(t)", which says that "term t is a proof of the proposition phi about t itself" - a self-referential assertion. Shown by Kuznets, such self-referential formulas are necessary in the translation of S4 in LP. By extending Kuznets' method, we are able to show that the same holds even for IPC. Interestingly, the set of IPC-theorems that indeed call for self-referentiality includes double negations of intuitionistic-invalid classical tautologies.

15:45-16:00　茶歇

16:00-16:45
报告六
报告人: 廖备水 浙江大学
题   目: Prioritised norms in formal argumentation
摘   要: In this talk, I will introduce a research about how to represent three approaches to reasoning with prioritised norms and defaults in formal argumentation. We show how a version of prioritised default logic and Brewka-Eiter's construction in answer set programming can be obtained in argumentation via the weakest and last link principles. We also show how to represent Hansen's recent construction by adding arguments using weak contraposition via permissive norms, and their relationship to Caminada’s ``hang yourself'' arguments. The advantage of the proposed approach is that it provides a way to study various properties of prioritized nonmonotonic reasoning in formal argumentation, in line with the idea proposed in Dung's seminal paper.

16:45-20:00　晚餐        详情请见　http://www.fengkui.me/delta_at_bnu/