Date/Time : 17 Jan 2024 17:00
Venue : S17 #04-05 (SR2)
Speaker : Makoto Tatsuta, National Institute of Informatics, Japan

An inductive definition is a way to define a predicate by an expression which may contain the predicate itself. The predicate is interpreted by the least fixed point of the defining equation. Inductive definitions are important in computer science, since they can define useful recursive data structures such as lists and trees.  Inductive definitions are important also in mathematical logic, since they increase the proof theoretic strength. Martin-Lof’s system of inductive definitions given in 1971 is one of the most popular system of inductive definitions. In 2006 Brotherston proposed an alternative formalization of inductive definitions, called a cyclic proof system. In general, for proof search, a cyclic proof system can find an induction formula in a more efficient way than Martin-Lof’s system, since a cyclic proof system does not have to choose fixed induction formulas in advance. The equivalence of the provability of Martin-Lof’s system for inductive definitions and that of the cyclic proof system was conjectured in 2006. The speaker and Berardi solved it in 2017.

This talk will explain this problem.

Add to calendar :

Date/Time : 09 Jan 2024 15:00
Venue : S17 #04-05 (SR2)
Speaker : Manlio Valenti, Swansea University

Ramsey’s theorem for n-tuples and k-colors can be generalized to colorings of binary trees. More precisely, TT^n_k states that given a k-coloring of the n-subsets of finite binary strings, there is a monochromatic set of strings that is isomorphic to the full binary tree. In the literature, this is sometimes referred to as
Chubb-Hirst-McNicholl tree theorem. In this talk, we will be focusing on the tree pigeonhole principle, namely the special case of the tree theorem for colorings of strings (i.e. n=1). We analyze its uniform computational content within the framework of Weihrauch reducibility. We show that different ways of phrasing the theorem yield different Weihrauch degrees. Our results provide new insights on the first-order part of the tree pigeonhole principle.

This is joint work with Damir Dzhafarov and Reed Solomon.

Add to calendar :

Date/Time : 05 Dec 2023 15:30
Venue : S17 #04-04 (SR3)
Speaker : Lu Qi, Princeton University

In this talk, I will discuss some convexity properties of multiplicities of filtrations on a local ring. In particular, the multiplicity function is convex along geodesics. As a major application, this gives a new proof of a theorem due to Xu and Zhuang on the uniqueness of normalized volume minimizers. In order to characterize strict convexity, we introduce the notion of saturation of a filtration, which turns out to be useful in other settings. For example, it allows us to generalizes a theorem by Rees on characterization of when two filtrations have equal multiplicities. It also allows us to introduce a metric on the space of filtrations. This talk is based on joint work with Harold Blum and Yuchen Liu and some ongoing work.

Add to calendar :

Date/Time : 14 Nov 2023 17:00
Venue : S17 #04-06 (SR1)
Speaker : Liu Shixiao,

Last semester I talked about the upper density Mathias forcing which we prove to be proper. This time we take a look at several similar forcings, each of which collapses the continuum to omega and thus fails to be proper.

Add to calendar :

Date/Time : 07 Nov 2023 17:00
Venue : S17 #04-06 (SR1)
Speaker : Ye Jinhe , University of Oxford

A difference field is a field equipped with a given automorphism and a difference variety is the natural analogue of an algebraic varieties in this setting. Complex numbers with complex conjugation or finite fields with the Frobenius automorphism are natural examples of difference fields.

For finite fields and varieties over them, the celebrated Lang-Weil estimate gives a universal estimate of number of rational points of varieties over finite fields in terms of several notions of the complexities of the given variety. In this talk, we will discuss an analogue to Lang-Weil estimate for difference varieties in finite difference fields. The proof uses pseudofinite difference fields, where the automorphism is the nonstandard Frobenius. This is joint work with Martin Hils, Ehud Hrushovski and Tingxiang Zou.

Add to calendar :

Date/Time : 31 Oct 2023 17:00
Venue : S17 #04-06 (SR1)
Speaker : Samuel Alfaro Tanuwijaya, National University of Singapore

The talk will deal with relativised versions of the Posner Robinson theorem and explore how far one can go and how to prove these relatived versions.

Add to calendar :

Date/Time : 24 Oct 2023 17:00
Venue : S17 #04-06 (SR1)
Speaker : Meng-Che Ho, California State University Northridge

Classically, the word problem of a group is the set of words equal to the identity of the group, and we analyze them using Turing reductions. In this talk, we consider the word problem of a group as a computably enumerable equivalence relation (ceer), namely, two words are equivalent if and only if they are equal in the group. We compare ceers using the computable reduction: $E$ is reducible to $F$ if there is a computable function $f$ so that $iEj$ if and only if $f(i)Ff(j)$.

We will discuss some recent results and see that the landscape of word problems as ceers is very different from the classical theory. For instance, in the classical setting, any Turing degree can be realized as a word problem by first constructing a countable group and then embedding it into a finitely presented group via the Higman embedding theorem. However, we prove that in the ceer setting, there is a group $G$ whose word problem is not universal, but for any nontrivial $H$, the free product $G*H$ has a universal word problem.

This is a joint work with Uri Andrews and Luca San Mauro.

Add to calendar :

Date/Time : 17 Oct 2023 17:00
Venue : S17 #04-06 (SR1)
Speaker : Frank Stephan, National University of Singapore

Floyd and Knuth studied in their 1990 paper addition machines which are machines which can add, subtract and compare integers (<,=,>) in unit time; also the reading or writing of an integer is in unit time. They showed that multiplying and dividing can be done in linear time with six registers and asked in their Open Problem (2) whether this bound can be broken; furthermore, they asked in Open Problem (5) of their paper whether there is a register machine which can output in subquadratic time the powers of two occurring in the binary representation of an integer.

The talk answers both questions affirmatively and presents the key ideas and programs to witness this.

Add to calendar :

Date/Time : 19 Sep 2023 17:00
Venue : S17 #04-06 (SR1)
Speaker : Neoh Tzeh Yuan,

The Boolean satisfiabilty problem (SAT) is a problem with great theoretical and practical interest. While heuristic algorithms tend to work well in practice, the widely believed strong exponential time hypothesis (SETH) conjectures that there is no deterministic algorithm for SAT in time O(c^n) for some constant c < 2. On the other hand, better bounds of O(c^n) with c < 2 have been found for various restricted (but still NP-complete) instances of SAT. One such problem is 3-Occur-SAT, where every variable in the formula occurs at most 3 times. Wahlstroem presented in 2005 an algorithm which solves the problem in time O(1.1279^n) and Peng and Xiao improved it (this year’s IJCAI) to O(1.1238^n).

I will present an algorithm that gives a further improvement to O(1.1199^n). I’ll discuss the common bottleneck cases faced by previous efforts and introduce new reduction and branching rules that can circumvent these cases.

The work I present is done in an internship at NUS / SOC supervised by Sanjay Jain and Frank Stephan from July to September 2023.

Add to calendar :