Complexity and Real Computation Laboratory

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

--- seminars [2022-05-29] – [2022] New Martin Ziegler
+++ seminars [2025-03-19] (current) – [Accelerating Operator Calculus] Martin Ziegler
@@ Line 1: / Line 1: @@
 ====== Seminar on Theoretical Computer Science, Logic, and Real Computation ======
+  * [[Seminars#2025]]
+  * [[Seminars#2024]]
+  * [[Seminars#2023]]
+  * [[Seminars#2022]]
   * [[Seminars#2021]]
   * [[Seminars#2020]]
@@ Line 9: / Line 13: @@
   * [[Seminars#2015]]
-===== 2022 =====
+===== 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 =====
+====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
+a series of tests for a braid being conjugate
+to a reducible braid, valid for every braid group.
+The method can be extended to exchangeable and
+composite braids and to Markov equivalence.
+We also determine the exact location of
+the eigenvalues of the Burau matrix (for suitable
+parameter), with those
+for reducible braids filling a complex disk and
+for the exchange move a Descartes oval.
+===== 2023 =====
+====Continuous Local Strategies for Robotic Formation Problems====
+===by Barbara Kempkes and Friedhelm Meyer auf der Heide (2012)===
+  * June 28, 19h KST
+  * Rakhman Ulzhalgas (KAIST)
+===== 2022 =====
 ====Computing with Infinite Objects via Coinductive Definitions====
@@ Line 16: / Line 108: @@
   * Dieter Spreen (U Siegen)
-Abstract:
+//Abstract://
-//A representation-free logic-base approach for computing with infinite objects will be presented. The logic is intuitionistic first-order logic extended by strictly positive inductive and coinductive definitions. Algorithms can be extracted from proofs via realizability. The approach allows to deal with objects like the real numbers and nonempty compact sets of such. More general, it allows to deal with compact metric spaces that come equipped with a finite set of contractions such that the union of their ranges covers the space, and with continuous maps between such spaces. The computational power of the approach is equivalent to that of type-two theory of effectivity.//
+A representation-free logic-base approach for computing with infinite objects will be presented. The logic is intuitionistic first-order logic extended by strictly positive inductive and coinductive definitions. Algorithms can be extracted from proofs via realizability. The approach allows to deal with objects like the real numbers and nonempty compact sets of such. More general, it allows to deal with compact metric spaces that come equipped with a finite set of contractions such that the union of their ranges covers the space, and with continuous maps between such spaces. The computational power of the approach is equivalent to that of type-two theory of effectivity.
+{{http://kaist.theoryofcomputation.asia/_media/screenshot_2022-06-02_152534.png}}
 ===== 2021 =====

Differences