On September 26, 2023, the VCLA will hold a combined award ceremony for the VCLA International Student Awards and the Helmut Veith Stipend 2022. The winners of the student awards will present their winning theses, and they will receive the award certificate. The Helmut Veith Stipend will be awarded to Ms. Alina Ehart by Kurt Matyas, TU Wien Vice Rector of Academic Affairs.

The event will take place one day prior to the MOSAIC Workshop 2023 at the same location. Anyone interested in attending the talks and Q&A sessions is very welcome to join us! After the ceremony, we will raise our glasses to the winners and enjoy some delicious Italian pastries.

Program

Speakers & Abstracts

Barbora Šmahlíková (Brno University of Technology)
“Next Generation of Rank-Based Algorithms for Omega Automata”

Büchi automata (BA) complementation is a crucial operation for termination analysis of programs, model checking, or decision procedures for various logics. Despite its prominence, practically efficient algorithms for BA complementation are still missing. This thesis deals with optimizations of Büchi automata complementation, focusing mainly on rank-based techniques. The original rank-based algorithm is asymptotically optimal, but it can still generate unnecessarily large state space. For a practical usage, it is therefore desirable to reduce the number of generated states in the complement as much as possible. We propose several techniques that can efficiently complement some special types of Büchi automata, occuring often in practice, based on their structure. Some of these techniques can also, to a certain degree, be extended to general Büchi automata. The developed techniques were implemented as an extension of the tool Ranker for Büchi automata complementation and evaluated on thousands of hard automata. Our optimizations significantly reduce the generated state space and Ranker produces in the majority of cases a smaller complement than other state-of-the-art tools.

Lydia Blümel (MA at the University of Leipzig, now a PhD student at FernUniversität in Hagen)
“Defining Defense in Abstract Argumentation from Scratch – A Generalizing Approach”

In my thesis, I show that the differences between various existing non-classical semantics for abstract argumentation can be captured in a single parameter – their defeat operator. A defeat operator can be any mapping from the power set of the argument set of an AF to itself. The main contribution is a generic framework for constructing argumentation semantics from a defeat operator. For this, I generalized Dung’s Gamma-Operator and his admissible, complete, preferred, grounded and stable semantics so that they are well-defined under any such mapping. I demonstrate that several existing semantics can be represented within this framework by choosing a suitable notion of defeat. The generic nature of my construction method allowed me to extend existing proposals in a natural way, e.g. by constructing the respective stable semantics from an adequate operator found and I discuss these new semantics as well as those generated from a genuinely new defeat operator. The satisfaction of existing principles by semantics generated with the new framework are discussed in general and depending on their defeat operator. Building on these insights new principles with a focus on the defense behaviour of a semantics are introduced. The findings of this work were presented at KR2022 [Blümel and Ulbricht, 2022]. To the best of my knowledge a generalized framework for argumentation semantics based on operators has not been proposed before.

Vitor Rodrigues Greati (MA at Universidade Federal do Rio Grande do Norte, now a PhD student at the University of Groningen)
“Hilbert-Style Formalism for Two-Dimensional Notions of Consequence”

The present work proposes a two-dimensional Hilbert-style deductive formalism (H-formalism) for B-consequence relations, a class of two-dimensional logics that generalize the usual (Tarskian, one-dimensional) notions of logic. We argue that the two-dimensional environment is appropriate to the study of bilateralism in logic, by allowing the primitive judgments of assertion and denial (or, as we prefer, the cognitive attitudes of acceptance and rejection) to act on independent but interacting dimensions in determining what-follows-from-what. In this perspective, our proposed formalism constitutes an inferential apparatus for reasoning over bilateralist judgments. After a thorough description of the inner workings of the proposed proof formalism, which is inspired by the one-dimensional symmetrical Hilbert-style systems, we provide a proof-search algorithm for finite analytic systems that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned system. We delve then into the area of two-dimensional non-deterministic semantics via matrix structures containing two sets of distinguished truthvalues, one qualifying some truth-values as accepted and the other as rejected, constituting a semantical path for bilateralism in the two-dimensional environment. We present an algorithm for producing analytic two-dimensional Hilbert-style systems for sufficiently expressive two-dimensional matrices, as well as some streamlining procedures that allow to considerably reduce the size and complexity of the resulting calculi. For finite matrices, we should point out that the procedure results in finite systems. In the end, as a case study, we investigate the logic of formal inconsistency called mCi with respect to its axiomatizability in terms of Hilbert-style systems. We prove that there is no finite one-dimensional Hilbert-style axiomatization for this logic, but that it inhabits a two-dimensional consequence relation that is finitely axiomatizable by a finite two-dimensional Hilbert-style system. The existence of such system follows directly from the proposed axiomatization procedure, in view of the sufficiently expressive 5-valued non-deterministic bidimensional semantics available for the mentioned two-dimensional consequence relation.