Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
seminars [2024-05-28] – [Implementation of the Burau spectral test] Martin Zieglerseminars [2025-03-19] (current) – [Accelerating Operator Calculus] Martin Ziegler
Line 1: Line 1:
 ====== Seminar on Theoretical Computer Science, Logic, and Real Computation ====== ====== Seminar on Theoretical Computer Science, Logic, and Real Computation ======
  
 +  * [[Seminars#2025]]  
   * [[Seminars#2024]]     * [[Seminars#2024]]  
   * [[Seminars#2023]]   * [[Seminars#2023]]
Line 11: Line 12:
   * [[Seminars#2016]]   * [[Seminars#2016]]
   * [[Seminars#2015]]   * [[Seminars#2015]]
 +
 +===== 2025 =====
 +
 +====Integer factorization of matrices and 4-dimensional genera of knots====
 +  * March 19, 9:15am KST 
 +  * N1 #601
 +  * Alexander Stoimenov (Dongguk U)
 +
 +This is a lecture, in which I explain
 +the methods for computing (smooth) 4-dimensional genera of knots,
 +based on signatures
 +and Donaldson's theorem, which leads to a criterion for the
 +integer factorization of Goeritz matrices. Here I will talk
 +about how to efficiently implement the search for such
 +factorizations.
 +I plan to show Chuck Livingston's KnotInfo site, and his notes on
 +my contributions to the computation of (smooth) 4-dimensional genera.
 +
 +====Automated Reasoning with Continuous Data====
 +  * March 19, 10:00am KST
 +  * N1 #601
 +  * Margarita Korovina (IIS SB RAS)
 +
 +In this talk we report on ongoing research on solving non-linear constraints
 +over the reals occurring in a wide range of applications, starting with program
 +verification, ranging over verification of real-world designs all the way to automation
 +of formally verified proofs of mathematical statements. In our framework
 +methods from Computable Analysis and Automated Reasoning are combined to
 +meet efficiency and expressiveness. This approach is applicable to a large number
 +of constraints involving computable non-linear functions, piecewise polynomial
 +splines, transcendental functions and solutions of polynomial differential equations.
 +We give an introduction to the **ksmt** calculus for checking satisfiability of
 +non-linear constraints in a CDCL style way inspired by advances in SAT solving.
 +Along proof search **ksmt** resolves two types of conflicts: linear and non-linear.
 +Linear conflicts are delegated to a decision procedure for linear real arithmetic
 +and non-linear conflicts are resolved by local linearisations separating the solution
 +set and the current conflict. We show that the ksmt calculus is a δ-complete
 +decision procedure for bounded problems. In this setting we discuss resent and
 +future research work.
 +
 +====From iRRAM to pyRRAM: Some thoughts on implementing real number arithmetic====
 +  * March 19, 10:45am KST  
 +  * N1 #601
 +  * Norbert Müller (Uni Trier)
 +
 +Due to their uncountability, real numbers have to be treated
 +completely
 +different compared to countable sets like the integer or even the
 +rational
 +numbers. In the talk we present basic ideas for implementations in
 +an existing
 +library written in C++ and in a derived current approach in
 +Python.
 +
  
 ===== 2024 ===== ===== 2024 =====
 +
 +====iRRAM for Knots====
 +  * September 26, 11h00 KST 
 +  * hybrid offline (N1 #524) + online (Zoom, ask for coordinates)
 +  * Jaden Jorradol (KAIST)
 +
 +Rehearsal for presentation of [[https://cs.kaist.ac.kr/research/techReport|KAIST Technical Report CS-TR-2024-428]] at [[https://www.lix.polytechnique.fr/CCC2024/|CCC'2024]].
  
 ====Implementation of the Burau spectral test==== ====Implementation of the Burau spectral test====
Line 18: Line 80:
   * hybrid offline (N1 #422) + online (Zoom, ask for coordinates)   * hybrid offline (N1 #422) + online (Zoom, ask for coordinates)
   * Alexander Stoimenov (Dongguk University)   * Alexander Stoimenov (Dongguk University)
 +  * Jaden Jorradol (KAIST)
  
 We use the spectrum of the Burau representation to introduce We use the spectrum of the Burau representation to introduce