| 2024 |
|---|
|
Tue, Dec 3 |
Mark Chimes |
Tree-Verifiable Graph Grammars |
internal |
|
- Time
- 11:00 am
- Location
- EI 6 Eckert
- Abstract
- In a context-free grammar, each production rule replaces a non-terminal symbol with a sequence of symbols, some of which may be non-terminals to be further expanded. This process repeats until all non-terminal symbols are replaced by terminal ones. Similarly, in a (context-free or hyperedge-replacement) graph grammar, each rule replaces a non-terminal hyperedge in a graph with a subgraph, which may itself contain further non-terminal hyperedges. The set of all possible end-results from such rules forms a language, which can often be characterized by a formula satisfied exactly by members of that language. The complexity of the grammar influences the complexity of these formulae: for instance, in the case of words, star-free languages correspond to those definable in first-order logic, while regular languages correspond to those definable in monadic second-order logic. For graphs, however, the situation is more complex. In our work, we introduce a special class of graph grammars, called "Tree-Verifiable Graph Grammars," and a new notion of bounded tree-width, called "Bounded Embeddable Tree-Width" and show that the languages generated by these tree-verifiable grammars are precisely those that are definable in Monadic Second-Order Logic with (Modular) Counting predicates and which have bounded embeddable tree-width.
In my talk, I will introduce the concept of graph grammars, briefly describe the intent of the "tree-verifiable" syntactic restriction, and mention the notion of tree-width without detailed explanation.
|
|
Thu, Nov 28 |
Clemens Hofstadler |
First-order theorem proving for operator statements |
guest |
|
- Time
- 11:00 am
- Location
- Seminarraum FAV EG B (Seminarraum von Neumann)
- Abstract
- Algebraic statements involving matrices or linear operators appear in various branches of mathematics and related disciplines. In linear algebra and geometry, we study matrices and their properties as fundamental objects, while in functional analysis, linear operators help to analyze function spaces. Their applications range from the study of integral and differential equations to different tasks in the field of signal processing. In quantum mechanics, linear operators describe the evolution of quantum systems through the Schrödinger equation.
In this talk, we present a recently developed framework [1] for proving first- order statements about identities of linear operators by performing algebraic computations with noncommutative polynomials. Our main result is a semi- decision procedure that allows to prove any true operator statement. We also discuss our SageMath software package operator gb, which offers functional- ity for automating such computations.
References
[1] Clemens Hofstadler, Clemens G. Raab, and Georg Regensburger. Uni- versal truth of operator statements via ideal membership. arXiv preprint, arXiv:2212.11662, 2024.
|
|
Wed, Nov 6 |
Márton Hajdu |
Efficient Term Ordering Checks with Ordering Diagrams |
internal |
|
- Time
- 11:00 am
- Location
- Seminarraum FAV 01 C
- Abstract
- Efficient calculi in saturation-based theorem proving such as the superposition calculus rely on simplification orderings on terms. Two of the most well-known such orderings are the Knuth-Bendix ordering (KBO) and the Lexicographic Path ordering (LPO). Despite having implementations running in linear time for KBO and in quadratic-time for LPO in the compared term sizes, performing several checks in sequence can still be a bottleneck. For example, comparing terms while trying to simplify newly derived clauses with a large set of unit equalities can easily take up most of the theorem prover's time. In this work, we introduce a novel indexing structure called the ordering diagram, which handles several term comparisons at once. By using lazy evaluation and information from previous comparisons, it scales well even for larger number of ordering checks. Ordering diagrams also offer the first fully runtime-specialized KBO and LPO implementations. Our implementation of ordering diagrams in the theorem prover Vampire has also contributed to Vampire's success in the 2024 version of CASC.
|
|
Mon, Oct 21 |
Rustan Leino |
Using Dafny to write correct programs |
guest |
|
|
|
Mon, Oct 21 |
Eva Maria Wagner |
Synthesis of Recursive Programs in Saturation |
internal |
|
- Time
- 11:00 am
- Location
- Seminarraum 366
- Abstract
- We turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction axioms and use them together with answer literals in saturation. We introduce new inference rules for induction in saturation and use answer literals to synthesize recursive functions from these proof steps. Our proof-of-concept implementation in the Vampire theorem prover constructs recursive functions over algebraic data types while proving inductive properties over these types. We show how our framework can synthesize challenging examples and discuss future work.
|
|
Mon, Jun 24 |
Joel Ouaknine |
The Skolem Landscape |
guest |
|
- Time
- 5:00 pm
- Location
- FAV HS2
- Abstract
- The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, its decidability has been open for nearly a century! In this talk, I will present a survey of what is known on the Skolem Problem and related questions, including recent and ongoing developments.
|
|
Wed, Apr 17 |
Byron Cook |
The Business of Proof |
guest |
|
|
|
Tue, Mar 26 |
Reiner Hähnle |
Context-aware Trace Contracts |
guest |
|
|
|
Tue, Feb 27 |
Florian Sextl |
Sound One-Phase Shape Analysis with Biabduction |
internal |
|
- Time
- 1:00 pm
- Location
- FAV HS2
|
|
Tue, Jan 30 |
Tobias Nießen |
Finding Counterexamples to Forall-Exists Hyperproperties |
internal |
|
- Time
- 1:00 pm
- Location
- FAV HS3 Zemanek
|
| 2022 |
|---|
|
Wed, Dec 14 |
Daniel Kröning |
Automated Reasoning at Amazon |
guest |
|
|
| 2021 |
|---|
|
Wed, Oct 20 |
Lutz Strassburger |
Combinatorial Proofs and Decomposition Theorems for First-order Logic |
guest |
|
|
|
Tue, Sep 21 |
Hans van Ditmarsch |
One Hundred Prisoners and a Light Bulb |
guest |
|
|
|
Thu, Jul 22 |
Joscha Bach |
Cognitive AI: From AI models to mental representations? |
guest |
|
|
|
Thu, Jan 14 |
Georg Gottlob |
Knowledge Processing, Logic, and the Future of AI |
guest |
|
|
| 2020 |
|---|
|
Tue, Jul 21 |
Cory Doctorow |
Working as Intended -- Surveillance Capitalism is not a Rogue Capitalism |
guest |
|
|
| 2019 |
|---|
|
Fri, Dec 13 |
Torsten Schaub |
Dynamic Answer Set Programming |
guest |
|
|
|
Wed, Dec 4 |
Joost-Pieter Katoen |
Probabilistic Programming: Machine Learning for the Masses? |
guest |
|
|
|
Wed, Nov 27 |
Dominique Larchey-Wendling |
Hilbert’s Tenth Problem in Coq |
guest |
|
|
|
Wed, Nov 20 |
Tommaso Moraschini |
Profinite Heyting algebras and the representation problem for Esakia spaces |
guest |
|
|
|
Mon, Nov 11 |
Prafullkumar Tale |
Lossy Kernels for Graph Contraction Problems |
guest |
|
|