KAML
세미나

2024년

2024년 제4회 가우스석학강연

  • 강연자: 김병한 (연세대학교)
  • 시간 및 장소: 2024년 11월 4일(월), 8일(금), 오후 4:00 ~ 5:30 / 서울대학교 상산수리과학관 129동 1층
  • 첫 번째 강연 제목: Compactness and ultraproducts in model theory
  • 초록: 수리논리 모델론의 근간이 되는 괴델의 compactness 정리를 소개하고 이를 ultraproduct라는 개념을 사용하여 증명하는 것이 강연의 목표다. 이의 응용으로, 수체 위에 정의된 elliptic curve들의 rank의 upper bound가 존재할 필요충분조건에 대한 이정욱 교수의 결과와, Ax의 pseudo finite field(ultraproduct of finite fields)에 관한 결과 등을 소개할 것이다.
  • 두 번째 강연 제목: Model theoretic studies on the real/complex fields, with exponentiation
  • 초록: 실수체에 대한 모델론 연구는 오랜 역사를 갖고 있다. 특히 Tarski의 real closed ordered field에 quantifier elimination이 있다는 결과는 시금석 역할을 하였다. 이의 증명을 소개하고 이를 바탕으로 Hilbert’s 17th problem(every positive definite rational function over the real field is a sum of squares of rational functions)을 쉽게 이끌어 낼 것이다. 여기에 exponentiation을 더한 구조에 대한 Wilkie 등의 모델론 연구를 소개할 것이다. 특히 그의 연구는 최근 Andre-Oort 예상이 완전히 해결되는 데 밑거름이 되었다. 시간이 된다면 Zilber의 complex field with exponentiation과 Schanuel의 예상과 관련한 모델론 연구도 소개하겠다.

24년도 창원 모델론 워크샵

  • 시간 및 장소: 2024년 10월 23일(수) ~ 2024년 10월 24일(목) / 국립창원대학교 32호관 308호
  • 주최자: 이정욱 (국립창원대학교)
  • 강연자: 김병한 (연세대학교), 백지선 (연세대학교), 이효윤 (연세대학교)
  • 강연 제목:
    • An introduction to Zilber’s pseudo-exponentiation
    • On the extremal number of face-incidence graphs
    • NIP theories and Szemeredi regularity lemma

A survey on topological semantics for provability logics

  • 강연자: Thomas Icard (Stanford University)
  • 시간 및 장소: 2024년 10월 7일(월), 오전 10:15 ~ 11:15 / 연세대학교 과학관 262호
  • 초록: This will be a survey of ideas and results on topological interpretations of provability logics, especially polymodal provability logics. Esakia first proved completeness for the basic Gödel-Löb logic of provability with respect to scattered spaces. Abashidze and Blass (independently) proved completeness w.r.t. a particular scattered space defined on the ordinal ω^ω​​. I will discuss older work of my own that extended the Abashidze-Blass result to a polymodal provability logic, which is complete with respect to a polytopological space on ϵ_0​​. I will then discuss more recent developments, including work by Beklemishev, Fernández, Joosten, Gabelaia, Aguilera, and others, generalizing and improving upon much of this.

Continuous combinatorics and natural quasirandomness

  • 강연자: Leonardo Nagami Coregliano (University of Chicago)
  • 시간 및 장소: 2024년 6월 4일(화), 오후 2:00 ~ 3:00 / 연세대학교 과학관 262호
  • 주최자: 이준경 (연세대학교)
  • 초록: The theory of graph quasirandomness studies several asymptotic properties of the random graph that are equivalent when stated as properties of a deterministic graph sequence. For example, a graph has all densities of finite subgraphs approximately equal to the random graph if and only if every linear-sized set has approximately the same edge density if and only if every linear-sized cut has approximately the same edge density.  

    Graph quasirandomness was also one of the main motivations for the theory of dense graph limits, also known as theory of graphons. Once developed, the theory of graphons provided further insight into graph quasirandomness with both new results and simpler proofs of existing ones.  

    The next step from graphons was the development of limits of arbitrary dense combinatorial objects, starting with ad hoc limits for hypergraphs, digraphs, tournaments and permutations and culminating in general limits of models of any universal first-order theory in a relational language, such as flag algebras and theons.  

    In parallel, several ad hoc theories of quasirandomness have been produced, which raised the question of whether these could be unified by a quasirandomness theory in the same general setting of models of universal theories of flag algebras and theons.  

    In this talk, I will briefly introduce the general theory of dense limits of combinatorial objects (often associated with the name continuous combinatorics) and talk about the notion of natural quasirandomness, a theory of quasirandomness in the same general setting of universal first-order theories as flag algebras and theons. The main concept explored by natural quasirandomness is that of unique coupleability, which roughly means that any alignment of two limit objects on the same ground set “looks random”.  

    No prior knowledge of quasirandomness, model theory or continuous combinatorics is necessary.  

    This talk is based on joint works with Alexander A. Razborov and with Henry Towsner.

Minimal operations over permutation groups

  • 강연자: Paolo Marimon (TU Wien)
  • 시간 및 장소: 2024년 3월 14일(목), 오후 2:00 ~ 3:00 / 고등과학원 1423호
  • 주최자: Javier De la Nuez Gonzalez (KIAS)
  • 초록: Joint work with Michael Pinsker. Let B be a fixed relational structure (e.g. a graph). The Constraint Satisfaction Problem for B, CSP(B), is the computational problem of, given a finite structure A in the same language, deciding whether there is a homomorphism from A into B. Many natural problems in computational complexity can be framed in this fashion. When the structure B is finite, we know that CSP(B) is always in NP, and, assuming P ≠​​ NP, we know that whether this problem is in P or NP-complete can be characterised in terms of identities satisfied by the polymorphisms of B (a higher arity generalisation of homomorphisms) (Bulatov 2017, Zhuk 2017). We are interested in generalising the tools used to study constraint satisfaction problems for finite structures to some infinite structures with many symmetries (finitely bounded homogeneous structures). Since understanding the polymorphisms of B is essential to understand the computational complexity of CSP(B), it is often helpful to find polymorphisms of low arity behaving in some non-trivial way. For this reason, we study what are called the minimal polymorphisms above the automorphism group of B. We carry out a classification of the types of minimal operations which may appear over an arbitrary permutation group G of B, generalising the work of Rosenberg (1986) for the trivial group and of Bodirsky and Chen (2007) for oligomorphic permutation groups. This allows us to answer some open problems mentioned by Bodirsky (2021) in his book on infinite domain CSPs.
  • KIAS 세미나 페이지

When measures don't care about structure (and when they do)

  • 강연자: Paolo Marimon (TU Wien)
  • 시간 및 장소: 2024년 3월 8일(금), 오후 4:30 ~ 5:30 / 연세대학교 과학관 254호
  • 초록: Joint work with Colin Jahel and Samuel Braunfeld. We study ways in which we can expand a homogeneous relational structure in a "random" way. The most basic example of this, studied by Ackerman, Freer and Patel (2016) and many others, are measures on the space of L-structures on a countable set which are invariant under the action of S∞. For a fixed homogeneous structure we study Aut(M)-invariant measures on the space of expansions of M to a language L'. Such measures have been previously studied by Crane & Towsner (2018) and Jahel & Joseph (2023). In particular, we are interested in the case of M being a homogeneous k-hypergraph, for which we study Aut(M)-invariant expansions by a lower arity hypergraph. Heavily modifying techniques of Angels, Kechris and Lyons (2014), we are able to prove that in various cases these Aut(M)-invariant measures are actually S∞-invariant. In particular, we manage to prove this also for some homogeneous structures M with free amalgamation but not satisfying disjoint n-amalgamation for all n. This was essentially out of the reach of previous work. Moreover, invariant Keisler measures on a given homogeneous structure are a special case of the context we study. Hence, we are able to describe the spaces of invariant Keisler measures for various homogeneous structures and show in many cases that the measure of a formula does not depend on the relations between its parameters. An especially important example is the generic tetrahedron-free 3-hypergraph, for which we prove that there are non-forking formulas which are universally measure zero. Finally, our techniques also provide an explanation for why the universal homogeneous two-graph has a unique invariant Keisler measure which is quite oddly behaved.

제3회 한국 논리학의 날 2024 (The 3rd Korea Logic Day 2024)

  • 시간 및 장소: 일시: 2024년 1월 12일 금요일 / Zoom online meeting
  • 주최: 한국논리학회
  • 조직위원: 최승락 (서울시립대학교, 주 조직위원), 김준희 (고등과학원), 박세원 (교토대학교), 이효윤 (연세대학교)
  • 등록: 2024년 1월 10일까지 google form을 통해 등록
  • 홈페이지: https://korealogicday.org/2024/kr/

2023년

Model Theory Conference in Seoul

  • 홈페이지: https://sites.google.com/yonsei.ac.kr/modeltheoryseoul2023/
  • 일시: 2023년 8월 28일(월) ~ 2023년 8월 30일(수)
  • 장소: 연세대학교 과학관 262호
  • 학회 소개: After the long period of pandemic, the Model Theory Conference will be held again in August 28-30, 2023 at Yonsei University in Seoul, Korea. The first Model Theory Conference was held at the same place in May, 2010. Then the Classification Theory Workshop took place at NIMS, Daejeon, Korea in August, 2014, and in July, 2017, the 15th Asian Logic Conference was held at NIMS as well.
    Yonsei University, established in 1915, has been the major source of model theory research in Korea since 2005. Today, model theory in Korea is spreading out to other places including Korea Institute for Advanced Study (KIAS). This success has motivated us to organize the upcoming conference. Yonsei University is located in Shinchon, a district known for its vibrant youth culture and art. We hope all the speakers and participants will enjoy experiencing various Korean cultures during the conference.
  • 강연자 목록: https://sites.google.com/yonsei.ac.kr/modeltheoryseoul2023/speakers
  • 등록 마감: 2023년 6월 15일
  • 후원: 연세대학교, 한국연구재단, Association for Symbolic Logic, Brain Korea 21, KIAS

Urysohn structures in continuous logic

  • 강연자: Su Gao (Nankai University)
  • 시간 및 장소: 2023년 6월 27일(화), 오후 4:30 ~ 5:30 / 연세대학교 과학관 254호
  • 초록: Continuous logic is a multi-valued logic for metric structures that has received a lot of attention in recent years. In this talk we consider questions in continuous model theory and give characterizations for the following properties in continuous logic: (1) the existence of Urysohn (pre-)structures; (2) the amalgamation property; (3) the existence of Fraisee limits for the class of finite continuous structures; (4) the EPPA property; (5) the existence of Fraisee limits for the class of finite group actions on finite continuous structures. This is joint work with Xuanzhi Ren.

Amenability, optimal transport and cohomology of Banach modules

  • 강연자: Christian Rosendal (University of Maryland)
  • 시간 및 장소: 2023년 6월 26일(월), 오후 4:30 ~ 5:30 / 연세대학교 과학관 254호
  • 초록: Using tools from the theory of optimal transport, we establish some new results concerning isometric actions of amenable topological groups. Specifically, consider an amenable topological group $G$ with no non-trivial homomorphisms to $\mathbb R$. Then, if $d$ is a compatible left-invariant metric on $G$, $E\subseteq G$ is a finite subset and $\epsilon>0$, there is a finitely supported probability measure $m$ on $G$ so that

    $$\max_{g\in E}\, W(m.g,m)<\eps,$$

    where $W$ denotes the Wasserstein or optimal transport distance between probability measures on the metric space $(G,d)$. When $d$ is the word metric on a finitely generated group $G$, this strengthens a well known theorem of H. Reiter. Furthermore, when $G$ is locally compact, $m$ may be replaced by an appropriate probability density $f\in L^1(G)$.

    Also, when $G\curvearrowright X$ is a continuous isometric action on a metric space, the space of Lipschitz functions on the quotient $X/\!\!/G$ is isometrically isomorphic to a $1$-complemented subspace of the Lipschitz functions on $X$. And finally every continuous affine isometric action of $G$ on a Banach space has a canonical invariant linear subspace. These results generalise previous theorems due to Schneider-Thom and Cúth-Doucha.

수학자를 위한 머신러닝

  • 강연자: 정주희 (경북대학교)
  • 시간 및 장소: 2023년 5월 26일(금), 오후 4:30 ~ 5:30 / 연세대학교 과학관 262호
  • 초록: 머신러닝은 수학자가 관심을 둘 법한 토픽이다. 불행하게도 머신러닝에 대하여 매스컴이나 도서에서 접하는 내용은 수학자가 이해하기 쉽지 않은 언어로 기술되어 있다. 게다가 주로 다루는 주제는 수학과 거리가 먼 편이다. 예를 들어 "머신러닝과 윤리", "머신러닝의 한계는 무엇인가?", "AI 시대에 도태되지 않으려면?" 등의 제목을 자주 보게 된다.

    우리는 이 강연에서 머신러닝에 대해서 수학자가 관심을 둘 만한, 그리고 잘 이해할 수 있을 만한 토픽 중의 일부를 수학자의 언어로 풀어 보고자 한다.

    구체적으로는 머신러닝 관련 글에서 자주 사용되고 중요한 다음의 용어들을 설명하려 한다.

    • 모델, 훈련, 추론, 예측
    • 로스함수(loss function), 엔트로피, 기울기 하강
    • 신경망, 딥러닝

    그리고 머신러닝의 실제 계산 과정을 보여주기 위하여 이미지 분류와 텍스트 분석에서 각각 기본적이고 대표적인 예를 하나씩 들어 볼 것이다.
    참고자료: https://colab.research.google.com/drive/1h2UvV75oIkxnrpmsx6sJWvqke5zf01Pm?usp=sharing


attachment:20230526_1.jpg



attachment:20230526_2.jpg


Minimality of some automorphism groups of homogeneous structures

  • 강연자: De la Nuez Gonzalez, Javier (KIAS)
  • 시간 및 장소: 2023년 5월 12일(금), 오후 4:30 ~ 5:30 / 연세대학교 과학관 262호
  • 초록: I will discuss joint work with Z. Ghadernezhad, where we show that under certain conditions the standard topology on the automorphism of a countable homogeneous structure (generated by the fixed point stabilizers of finite sets) is minimal among the Hausdorff group topologies on the group. I will also touch upon related results in the context of (generalized) Urysohn spaces.

2022년

직관주의적 유형론에서의 분석성과 결정가능성 및 완전성

  • 강연자: 정인교 (고려대학교)
  • 시간 및 장소: 2022년 9월 30일(금), 오후 3:30 ~ 4:30 / 연세대학교 과학관 254호
  • 초록: 마틴뢰프(Per Martin-Löf)는 판단의 형식들에 관한 그의 직관주의적 유형론(Intuitionistic Type Theory)에서의 분석에 의거하여 다음과 같은 주장을 한다.

    논리 법칙들에 해당하는 통상적인 판단들과 수학의 통상적인 판단들은 대부분 분석판단(analytic judgement)이 아니라 종합판단(synthetic judgement)이다.
    분석판단과 종합판단의 구분은 결정불가능성(undecidability)과 불완전성(incompleteness)의 현상을 제대로 이해하기 위해 매우 중요하다; 분석판단의 논리는 결정가능하며 완전하지만, 종합판단의 논리는 결정불가능하고 불완전하다.

    본 발표에서는 마틴뢰프의 주장들이 의존하는 개념들을 분명히 하고, 그의 주장들을 검토할 것이다. 특히, 직관주의적 유형론에 의거한 그의 분석판단과 종합판단의 구분이 적절한 것인지, 기존의 구분들과 비교해 검토될 것이다.

The Place of Mathematical Logic in the 20th Century American Mathematics: Mac Lane’s Perspective

  • 강연자: 박우석 (KAIST)
  • 시간 및 장소: 2022년 9월 30일(금), 오후 4:40 ~ 5:40 / 연세대학교 과학관 254호
  • 초록: Even though mathematical logic does have its place in the classification of mathematics, it is by no means clear what role it should play in mathematics. After all these years, there is still doubt as to whether mathematical logic is considered to be genuine mathematics by most mathematicians. Understanding this unfortunate situation is a thorny issue, which invites the invocation of the entire history of the classification of mathematics, science, and philosophy. In this paper, my modest aim is merely fathoming the place of mathematical logic in the history of 20th century American universities through Saunders Mac Lane’s perspective. In as much as his life (or work) is uniquely multi-faceted, at least some useful springboards for promoting the fruitful dialogues between mathematicians, philosophers, and mathematical logicians could be secured from this discussion.

attachment:20220930_1.jpg



attachment:20220930_2.jpg


제2회 한국 논리학의 날 2022 (The 2nd Korea Logic Day 2022)

The Connes Embedding Problem, MIP*=RE, and Model Theory

  • 강연자: Prof. Isaac Goldbring (University of California, Irvine)
  • 일시: 2022년 1월 5일(수) ~ 2월 23일(수), 매주 수요일 11:00 ~ 12:20, 총 8회
  • 장소: Zoom online meeting
  • 초록: The Connes Embedding Problem (CEP) is arguably one of the most famous open problems in operator algebras. Roughly, it asks if every tracial von Neumann algebra can be approximated by matrix algebras. In early 2020, a group of computer scientists proved a landmark result in quantum complexity theory called MIP*=RE and, as a corollary, gave a negative solution to the CEP. However, the derivation of the negative solution of the CEP from MIP*=RE involves several very complicated detours through C*-algebra theory and quantum information theory. In this series of lectures, I will present the "standard" derivation of the failure of CEP from MIP*=RE. In addition, I will present joint work with Bradd Hart where we show how some relatively simple model-theoretic arguments can yield a direct proof of the failure of the CEP from MIP*=RE while simultaneously yielding a stronger, Gödelian-style refutation of CEP as well as the existence of "many" counterexamples to CEP. I will assume no prior knowledge of operator algebras, quantum complexity theory, or model theory and will try to develop as much of the story from scratch as possible.
  • 강의에 대한 정보 사이트: https://www.math.uci.edu/~isaac/yonsei.html

2021년

제1회 한국 논리학의 날 2021 (The 1st Korea Logic Day 2021)

2019년

Coordinatization of Lattices and the Noncommutative Zariski Spectrum

  • 강연자: Ivo Herzog (Ohio state University)
  • 시간 및 장소: 2019년 5월 10일(금) 오후 4:30 ~ 5:30 / 연세대학교 과학관 254호
  • 초록: In the model theory of modules over a ring R, the most important formulae are the positive primitive formulae, whose logic is reminiscent of the quantum logic introduced by von Neumann to formalize deductive reasoning of statements about quantum phenomena. We will describe the formalism of positive primitive formulae, and how it can be used to generalize von Neumann's program to coordinatize complemented modular lattices by (von Neumann) regular rings. A precise result is obtained by relativizing the lattice to a universal quotient lattice, with respect to the unique complement property (UCP). This quotient lattice is coordinatized by the universal abelian regular ring over R, whose Pierce sheaf is a noncommutative version of the Zariski spectrum of R, equipped with the patch, or constructible, topology. This is joint work with S. L'Innocente.

Existence of antichain trees in SOP1-NSOP2 theories

  • 강연자: 김준희 (연세대학교)
  • 시간 및 장소: 2019년 12월 20일(금), 오후 4:00 ~ 4:50 / 연세대학교 과학관 227호
  • 초록: We introduce a notion of tree indiscernibility which holds for witness of SOP1. From this, we construct an antichain tree in SOP1-NSOP2 whose existence implies SOP1 and TP2. If there exists a theory having SOP1 property but not SOP2, then the theory has an antichain tree. And any tree indiscernibility whose tree language can expresses imcomparable relation (for example str-indiscernibility, s-indiscernibility) holds for any antichain tree. This is a joint work with JinHoo Ahn.

Elementary equivalence theorem for PAC structures

  • 강연자: 이정욱 (Wrocław University)
  • 시간 및 장소: 2019년 12월 20일(금), 오후 5:00 ~ 6:00 / 연세대학교 과학관 227호
  • 초록: We introduce a notion of PAC structures, which generalizes perfect PAC fields and we provide an elementary equivalence theorem for PAC structures. It is well known that elementary equivalences of PAC fields are controlled by their Galois groups: For given two PAC fields, if their Galois groups are isomorphic over Galois group over Galois group over a common subfield, then two PAC fields are elementary equivalent. The Key ingredient of this result is the Embedding Lemma for PAC fields, proved by M. Jarden and U. Kiehne. We generalize Embedding Lemma for PAC fields into PAC structures and using our generalized Embedding Lemma, we deduce the elementary equivalence theorem for PAC structures. This is a joint work with J. Dobrowolski and D. M. Hoffmann.

2018년

Two topologies of the Lascar group and the type-definability of orbit equivalence relations

  • 강연자: 이효윤 (연세대학교)
  • 시간 및 장소: 2018년 6월 22일(금) 오후 4:00 ~ 4:50 / 연세대학교 과학관 254호
  • 초록: In this talk, I will introduce the Lascar group of a complete theory and its two (equivalent) topologies. Then I will pointout that the original topology defined in terms of ultraproduct still comes useful, for example in showing the type-definability of certain orbit equivalence relations.

Interpreting type theory: the realizability way

  • 강연자: 이소리 (University of Cambridge, UK)
  • 시간 및 장소: 2018년 6월 22일(금), 오후 5:00 ~ 6:00 / 연세대학교 과학관 254호
  • 초록: Type theory is a band of formal systems that has its roots in the foundations of mathematics, and has been an essential object of study in theoretical computer science. In the last decade it has drawn yet another wave of attention for its connection with algebraic topology and higher category theory. This talk will be an introduction to type theory, with the goal of illuminating particularly the last aspect in a natural manner. Building upon our understanding of ordinary predicate logic and its set-theoretic semantics, formal systems such as many-sorted predicate logic, storied type theory (work in progress) and dependent type theory will be gradually illustrated in parallel with their semantics. Storied type theory serves as a bridge between many-sorted logic and dependent type theory. This work emerged from attempts to bring over a particular model construction in many-sorted logic to dependent type theory. The model construction is some fundamental ingredient in categorical realizability, which if time permits may be discussed, for it provides us with concrete non-trivial models of type theory.

Omega-categorical inp minimal groups, rings, and bilinear forms

  • 강연자: Jan Dobrowolski (University of Leeds, UK)
  • 시간 및 장소: 2018년 5월 25일(금), 오후 2:00 ~ 2:45 / 연세대학교 과학관 254호

Understanding the Curry-Howard Correspondence via Coq

  • 강연자: 정주희 (경북대학교)
  • 시간 및 장소: 2018년 5월 25일(금), 오후 3:00 ~ 4:00 / 연세대학교 과학관 254호

수학, 논리학 그리고 '한계'의 철학

  • 강연자: 박창균 (서경대학교)
  • 시간 및 장소: 2018년 5월 25일(금), 오후 4:20 ~ 5:20 / 연세대학교 과학관 254호

2017년

한국정보과학회 프로그래밍언어연구회 겨울학교 (SIGPL Winter School 2017)

  • 강연자: 허충길 (서울대학교), Martin Ziegler (KAIST)
  • 일시: 2017년 2월8일(수) ~ 2017년 2월10일(금)
  • 사전등록 마감: 2월 5일
  • 장소: KAIST 정보전자공학동(E3-1) 1층 제1공동강의실 (1501호)
  • 주최: 한국정보과학회 프로그래밍언어연구회
  • 주관: KAIST SW 중심 대학
  • 개요: 정형 증명 도구 Coq를 이용하여 논리학의 정리 증명 이론을 프로그래밍하고 실습합니다. 프로그래밍언어, 정형 기법, 시스템의 검증과 안전성, 그리고 전산학의 기초 이론 분야에 관심 있는 분들의 많은 참여 바랍니다.
  • 홈페이지: http://sigpl.or.kr/school/2017w

Kim-Independence and NSOP1 Theories

  • 강연자: Nick Ramsey (UC Berkeley)
  • 시간 및 장소: 2017년 1월 11일(수), 13일(금), 14:00 ~ 17:00 / 연세대학교 과학관 254호
  • 초록: The success of the theory of simple theories is built upon a number of theorems showing that forking has many desirable properties in a simple theory. Most of these properties, moreover, characterize simplicity (e.g., symmetry, transitivity, Kim's lemma), which means that a naïve generalization of these theorems to a broader class of theories is impossible. We will describe some recent work, now joint with Itay Kaplan, which shows that a simplicity-style structure theory exists for NSOP1 theories after replacing forking and dividing with their generic analogues, Kim- forking and Kim-dividing. This yields many new characterizations of NSOP1 theories and generalizes the known independence theory in several key examples.
  • 강연 슬라이드: 여기

2016년 2학기

Verification in Real Computation

  • 강연자: 박세원 (KAIST)
  • 시간 및 장소: 2016년 11월 4일, 금요일, 16:30 ~ 17:30시 / 연세대학교 과학관 263호
  • 초록: Using fundamental ideas from [Brattka&Hertling'98] and by means of object-oriented overloading of operators, the iRRAM library supports imperative programming over the reals with a both sound and computable, multivalued semantics of tests. We extend Floyd-Hoare Logic to formally verify the correctness of symbolic-numerical algorithms employing such primitives for three example problems: truncated binary logarithm, 1D simple root finding, and solving systems of linear equations. This is to be generalized to other hybrid (i.e. discrete and continuous) abstract data types.

  • 강연 슬라이드: 여기

Contemporary Model Theory

  • 강연자: Prof. Anand Pillay (Univ. of Notre Dame)

  • 시간 및 장소: 2016년 12월 16일, 금요일, 16:30 ~ 17:30시 / 연세대학교 과학관 262호
  • attachment:20161216_0.jpg

  • attachment:20161216_1.jpg

  • attachment:20161216_2.jpg

2016년 1학기

Logical Foundations of Efficient Validated Numerics

  • 강연자: Prof. Martin Ziegler (KAIST)

  • 시간 및 장소: 2016년 8월 26일, 금요일, 16:30 ~ 17:30시 / 연세대학교 과학관 262호
  • 초록: Recursive Analysis as the synthesis of computability theory and real analysis provides a sound foundation to Validated Numerics, that is, computation over real numbers and other continuous universes by approximation up to arbitrary guaranteed absolute error. In this talk I will recall its basic concepts and results before proceeding to its resource-bounded refinements, that is, address questions of algorithmic efficiency for real functions as investigated by Harvey Friedman, Ker-I Ko, Katrin Tent, and (the other) Martin Ziegler from Freiburg; I will conclude with recent own results about ordinary differential equations, about operators on analytic functions, and about computation on arbitrary compact metric spaces.
  • 강연 슬라이드: 여기

2015년 2학기

Frege's influence on modern practice of mathematics and logic

  • 강연자: 이계식 교수 (한경대학교)

  • 시간 및 장소: 2016년 2월 26일, 금요일, 17 ~ 18시 / 연세대학교 과학관 225호
  • 초록: This work started with the observation that, in Frege's work such as 'Begriffsschrift' and 'Basic Laws of Arithmetic', parameters (also called free variables) play essentially no role. And this drove us to check whether we could show the same meta-theoretic results even when we do not involve parameters to the language. We introduce a representation style of variable binding which is an important factor in doing formal proofs by using a computer. Our representation is a variation of the Coquand-McKinna-Pollack's locally-named representation. The main characteristic of our representation is the use of dependent families in defining expressions such as terms and formulas. We also show some hidden utility of simultaneous substitution and simultaneous renaming. Moreover, we could reveal a new aspect of locally-named representation style that it can be regarded as a nominal approach under the condition that proofs-as-programs is not a part of the domain of the discourse.

  • 강연 슬라이드: 여기

2015년 1학기

Point-free foundation of Mathematics

  • 강연자: Marco Benini 교수 (Università degli Studi dell’Insubria, 이탈리아)

  • 시간 및 장소: 2015년 7월 21일, 화요일, 16 ~ 17시 / 연세대학교 과학관 225호
  • 초록: In this talk, an alternative semantics for first-order, intuitionistic based theories is introduced. It main feature is to be "point-free", i.e., not requiring a universe where to interpret terms to exist. This semantics is sound and complete, and has many links with existing semantics. It fits into the paradigm "Correcteness by Construction" since it allows a direct computational interpretation of proofs along the lines of the propositions-as-types correspondence.
  • 강연 슬라이드: 여기

Mechanization of Proof: From 4-Color Theorem to Compiler Verification

  • 강연자: 허충길 교수 (서울대학교 컴퓨터공학부)

  • 시간 및 장소: 2015년 6월 5일(금요일), 17 ~ 18시 / 연세대학교 과학관 225호
  • 초록: 여기

2014년 2학기

컴퓨터과학자가 파악한 튜링의 원조논문 (Readings of Turing's 1936 Paper)

  • 강연자: 이광근 교수 (서울대학교 컴퓨터공학과)

  • 시간 및 장소: 2015년 7월 21일, 화요일, 16 ~ 17시 / 연세대 과학관 225호

Curry-Howard Isomorphism

  • 이계식 교수 / 매주 금요일 14 ~ 16시 / 연세대학교 과학관 221호

  • 교재: M. Sørensen and P. Urzyczyn, "Lectures on the Curry-Howard Isomorphism"

  • 내용: 주제는 Curry-Howard isomorphism이지만 유형론과 증명론 전반에 대한 소개를 다룹니다.
    • Type-free Lambda calculus, Intuitionistic logic, Simply typed Lambda calculus, Curry-Howard Isomorphism, Classical logic and control operator, First-order logic/arithmetic, Second-order logic/arithmetic and polymorphism, Dependent types

2013년 2학기

Type-amalgamation properties and polygroupoids in stable theories

  • 강연자: 김병한 교수 (연세대학교 수학과)

  • 시간 및 장소: 2013년 10월 11일, 금요일, 16 ~ 17시 / 경북대학교 자연과학대학 102호
  • 초록: We define a family of complete totally categorical first-order theories indexed by n ≥ 2 such that the nth theory has k-uniqueness property for all k ≤ n but fails to have (n+1)-uniqueness. The theories axiomatize structures that are relatives of polyadic groups. We show that such structures must be interpretable in any first-order theory that has k-uniqueness for all k ≤ n but fails (n + 1)-uniqueness. As an application, we give a more precise classification of totally categorical theories of disintegrated type. This is a joint work with John Goodrick and Alexei Kolesnikov.

2013년 1학기

Elementary Patterns of Resemblance

  • 강연자: Gunnar Wilken 박사 (Oist Institute of Science and Technology)
  • 시간 및 장소: 2013년 6월 28일, 금요일, 16:00~17:00 / 연세대학교 과학관 225호
  • 초록: In the first half of my talk, I will talk about the history of proof theory. Then Tim Carlson's access pattern will be introduced. At the end I try to give an overview of describing ordinals with patterns.

모델론에서의 호몰로지군론과 1-껍질을 갖는 2-사슬들의 분류

  • 강연자: 이정욱 (연세대학교 수학과 박사과정)
  • 시간 및 장소: 2013년 4월 19일, 금요일 18:00~19:00 / 연세대학교 과학관 225호

역수학과 증명보조기 (Reverse mathematics and proof assistants)

  • 강연자: 이계식 교수 (한경대학교 웹정보공학과)
  • 시간 및 장소: 2013년 3월 13일, 수요일 17:00~18:00 / 연세대학교 과학관 221호

2012년 2학기

An Example of Logic in Computer Science : Certified Programming with Dependent Types (Part 2)

  • 강연자: 차리서 (고려대학교 컴퓨터·전파통신공학과 박사과정)
  • 시간 및 장소: 2012년 12월 7일, 금요일 16:00~17:00 / 연세대학교 과학관 325호

An Example of Logic in Computer Science : Certified Programming with Dependent Types

  • 강연자: 차리서 (고려대학교 컴퓨터·전파통신공학과 박사과정)
  • 시간 및 장소: 2012년 11월 16일, 금요일 오후 16:00~17:00 / 연세대학교 과학관 227호

2012년 1학기

증명과 계산

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2012년 2월 10일, 금요일 오후 16:00~17:00 / 연세대학교 과학관 227호

2010년 2학기

수학혁명과 논리

  • 강연자: 박창균 교수 (서경대학교 철학과)
  • 시간 및 장소: 2012년 11월 26일, 금요일 16:00-17:00 / 연세대학교 과학관 225호

2009년 2학기

Forcing, and the Independence of the Continuum Hypothesis: A talk in memory of Cohen

  • 강연자: 김병한 교수 (연세대학교 수학과)
  • 시간 및 장소: 2009년 11월 24일, 화요일 16:00-17:00 / 연세대학교 과학관 225호

Formal proof - Theory and practice

  • 강연자: 기계식 박사 (ROSAEC Center, Seoul National University)
  • 시간 및 장소: 2009년 9월 28일, 월요일 15:00-16:00 / 연세대학교 과학관 225호
  • 초록: A language is a set of symbols each of which has a kind of fixed rule for its use. These rules form the grammar of the language. Following the grammar, one builds formulas and proof systems. A formal language is a language for which there is a purely mechanical process for proofs or verification of a mathematical property. And a formal proof is a proof written in a formal language which can be easily checked by its mechanical process.

In this talk an overview of the current state in formal proof will be given. The main contents are based on the four papers of the Notices of the American Mathematical Society published in November 2008.(http://www.ams.org/notices/200811/index.html)

Decidability and Elimination of Quantifiers

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2009년 9월 25일, 목요일 11:00~12:00 / 연세대학교 과학관 225호

2009년 1학기

Fast growing functions and logic

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2009년 3월 23일, 금요일 14:00~15:00 / 연세대학교 과학관 225호

2008년 2학기

Leibniz's Logic

  • 강연자: 박창균 교수 (서경대학교 철학과)
  • 시간 및 장소: 2008년 11월 20일, 목요일 11:00~12:00 / 충북대학교 자연과학대학 수학과 대학원 강의실 (40동 412호실)

귀납적 정의의 집합론적 근거 (Set-theoretic basis of Inductive definitions)

  • 강연자: 이계식 박사 (National Institute of Advanced Industrial Science and Technology (AIST)
  • 시간 및 장소: 2008년 6월 13일, 금요일 11:00~12:00 / 연세대학교 과학관 B130호
  • 초록: 수학 및 논리학에서 일상적으로 사용되는 귀납적 정의는 정의 되는 집합을 구성하는 원소를 생성하는 규칙의 집합으로 표시되며 정의 되는 집합의 어떤 원소도 주어진 규칙에 의거하여 생성된다고 규정한다. 자연수의 집합이 대표적인 예이며 모든 형식언어(formal languages)에서 기본적으로 사용된다. 이번 강연에서는 귀납적 정의의 집합론적 근거와 활용을 살펴본다. Inductive definitions, which are routinely used in mathematics and logic, can be described as a collection of rules that generate the elements of the sets to be defined. And inductive definitions declare that every element of the set be generated only via these rules. Inductive definitions are routinely used in every formal language. The set of natural numbers is a good example. In this lecture, we discuss the set-theoretic basis and applications of inductive definitions.

2007년 2학기

Topology and Computation

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2007년 12월 18일, 화요일 11:00~12:00 / 연세대학교 과학관 B102호

Ultraproduct and Compactness

  • 강연자: 김선영 (연세대학교 수학과 박사과정)
  • 시간 및 장소: 2007년 12월 7일, 금요일 15:30~17:00 / 연세대학교 과학관 246호

Introduction to the Model Theory of Modules: Positive-primitive formulae

  • 강연자: Ivo Herzog 교수 (연세대학교 수학과)
  • 시간 및 장소: 2007년 9월 21일 ~ 11월 30일, 매주 금요일 15:30~17:00 / 연세대학교 과학관 246호
  • 내용: The first lecture will be devoted to the formal calculus of positive-primitive (pp-) formulae, and the early results in the theory. This will include Baur's elimination of quantifiers up to pp-formulae and the axiomatization of complete theories in terms of invariants statements. Examples from abelian groups will be described.

증명론과 컴퓨터수학 (Proof theory and computer mathematics)

  • 강연자: 이계식 박사 ((ROSAEC Center, Seoul National University)
  • 시간 및 장소: 2007년 9월 14일, 금요일 13:00~14:00 / 연세대학교 과학관 B130호