Seminars

Wednesday, March 27, 2024: Simon Guilloud (EPFL)

Time: 10:15 - 11:00
Location: BA 607 (Bajuwarenstrasse 4, 6th floor) and https://uni-regensburg.zoom-x.de/j/9999678980
 

Title: Using Orthologic in Automated Reasoning

Abstract: Orthologic is a logical system whose underlying algebra is that of ortholattices (relaxations of boolean algebras which don't necessarily satisfy the distributive law). Because validity of formulas in orthologic can be decided in polynomial time, we are interested in their applicability to efficient and predictable automated reasoning. This talk will present a collection of algorithmic and logical results about orthologic, and explain how it was implemented in the program verifier Stainless and the proof assistant Lisa.

Thursday, November 30, 2023: Julie Cailler (University of Regensburg)

Time: 10:15 - 11:00
Location: BA 607 (Bajuwarenstrasse 4, 6th floor) and https://uni-regensburg.zoom-x.de/j/64045918898
 

Title: Designing an Automated Concurrent Tableau-Based Theorem Prover for First-Order Logic

Abstract: Automated Theorem Proving (ATP) involves the use of formal methods to automatically (dis)prove logical formulas. Its primary applications include bug detection in critical systems and assistance in demonstrating mathematical proofs.

This talk focuses on the presentation of Goéland, a concurrent automated theorem prover, and the main challenges it encounters. These challenges include implementing a fair tableau-based proof-search procedure, addressing theory reasoning, and ensuring the generation of machine-checkable proofs.

Thursday, November 16, 2023: Franziska Alber (University of Regensburg)

Time: 10:15 - 11:00
Location: BA 607 (Bajuwarenstrasse 4, 6th floor) and https://uni-regensburg.zoom-x.de/j/62895178597
 

Title: Complementation of Parametric Finite State Automata

Abstract: Finite State Automata (FSAs) are a well-researched model of computation where each FSA corresponds to a regular language. In particular, determinisation and complementation are well-understood: while a FSA may be nondeterministic, it is always possible to construct an equivalent deterministic FSA and use this construction to find a FSA that corresponds to the complement language.

Parametric Automata (PAs) are a generalization of finite state automata that are suited for handling infinite alphabets (and therefore, a wider array of formal languages). Transitions do not simply compare fixed letters, but may contain logical formulae or compare the input to nondeterministically assigned parameters. This increased power comes at a price: there is no definite, canonical way to define determinism for PAs, and unlike FSAs, PAs are not closed
under complementation (i.e., a complement may not exist!). We will explore different kinds of determinism for PAs and define several classes of PAs that can effectively be complemented.