Computational Logic Seminar

General Information

This is the website of the research seminar of the Computational Logic Group at the Institute of Discrete Mathematics and Geometry of TU Wien. The seminar usually takes places on Wednesdays from 10:00 to 11:00 in the seminar room DC red 07. The seminar is organised by J. Aguilera, E. Fokina and S. Hetzl.

If you want to receive talk announcements by e-mail, please subscribe to the mailing list of this seminar on its administration page.

October 7, 2026: Johannes Weiser (TU Wien)
title: Comparing Explicit and Implicit Methods for Solving CHCs
abstract:
Constrained Horn Clauses (CHCs) can be considered to be an intermediate representation language of (recursive) computer programs and assertions about them. Similar to programs, they can be executed symbolically. In this talk, we present algorithms for symbolically executing CHCs in both forward and backward direction. These are implicit methods since they do not produce an explicit invariant of the system. We show how to construct an explicit invariant after either symbolic execution algorithm terminates, even in the case of nonlinear clauses. We compare our algorithms with explicit methods that produce invariants. We show that all of these methods (forward execution, backward execution, searching for explicit quantifier-free invariants) are pairwise incomparable.

October 14, 2026: Franziskus Wiesnet (TU Wien)
title: On the Limits of Recursive Characterizations in the Refined A-Translation
abstract:
The refined A-translation, due to Berger, Buchholz, and Schwichtenberg, is based on recursively defined classes of formulas in minimal arithmetic, in particular the classes of definite and goal formulas. Schwichtenberg and Wainer observed that one of the key proof-theoretic properties of definite formulas also holds for formulas outside the original class and asked whether all formulas satisfying this property admit a useful characterization.
In this talk, I show that this is not possible. More precisely, none of the four proof-theoretic properties associated with the formula classes in the refined A-translation admits a recursive characterization. We will also show how the original framework can nevertheless be extended, and present an extended formulation of the refined A-translation including conjunction.