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-27] – 2024 June: Stoimenov 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 =====
-* June 4, 13h30 KST 
-* Alexander Stoimenov (Dongguk University) 
  
-*//Implementation of the Burau spectral test//*+====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==== 
 +  * June 4, 13h30 KST 
 +  * hybrid offline (N1 #422) + online (Zoom, ask for coordinates) 
 +  * 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
 a series of tests for a braid being conjugate a series of tests for a braid being conjugate
Line 30: Line 95:
 ===== 2023 ===== ===== 2023 =====
  
-* June 28, 19h KST +====Continuous Local Strategies for Robotic Formation Problems==== 
-* Rakhman Ulzhalgas (KAIST) +===by Barbara Kempkes and Friedhelm Meyer auf der Heide (2012)=== 
 + 
 +  * June 28, 19h KST 
 +  * Rakhman Ulzhalgas (KAIST) 
  
-"//Continuous Local Strategies for Robotic Formation Problems//" 
-by Barbara Kempkes and Friedhelm Meyer auf der Heide (2012) 
  
 ===== 2022 ===== ===== 2022 =====