World Logic Day 2024
Department of Computer Science, University of Oxford
12th January 2024, Lecture Theatre A, Wolfson Building
Department of Computer Science at the University of Oxford will celebrate the UNESCO World Logic Day together with a number of academic institutions all around the world!
On this occasion on 12th January 2024 in an in-person session three esteemed senior researchers will offer a closer look at their fields of research and explain how logic and logical methods are exploited therein. The event will consist of the following up-to-1-hour live talks, each one followed by a short discussion. The talks will be aimed at students and researchers in logic, computer science and mathematics, and everyone is welcome to attend. Participation is free of charge, and no pre-registration is required.
For online attendance, click here (can be opened in a browser on desktop, no app required in this case).
Schedule:
13:30-14:30
Linear Temporal Logics on Finite Traces
In this talk we look at temporal logics on traces that are assumed to be finite, as typical of action planning in Artificial Intelligence and of process modeling in Business Process Management. Having to deal with finite traces has been considered a sort of accident in much of the AI and BPM literature, and standard temporal logics (on infinite traces) have been hacked to fit this assumption. Only recently a specific interest in studying the impact of such an assumption emerged. We will survey linear temporal logics on finite traces, including LTLf, LDLf, and pure-past LTL, reviewing the main results on Satisfiability, Verification, and Synthesis. The talk will also draw connections with work in AI Planning, Non-Markovian Decision Processes, Reinforcement Learning, and BPM Declarative Process Modeling. The main catch is that working with these logics can be based on the manipulation of regular automata on finite strings, simplifying greatly reasoning and especially synthesis.
14:30-15:00
Break
15:00-16:00
Making elementary decisions about natural numbers
This talk will be an introduction to logical theories of arithmetic given from a discrete mathematics and computer science perspective. In particular, I will talk about:
* periodic and ultimately periodic sets of natural numbers,
* how to decide the truth value of logical statements that involve linear inequalities, Boolean connectives, and quantifiers that range over natural numbers (formally: in the first-order theory of natural numbers with addition),
* how these ideas and methods extend to other arithmetic theories (including some recent research results).
16:00-17:00
On unambiguous finite automata
Finite automata are fundamental for automated verification. A nondeterministic finite automaton is called unambiguous if every accepted word has only one accepting run. Thus, unambiguous automata are in between deterministic and nondeterministic automata. They are naturally connected to linear algebra and combinatorics. The infinite-word version of unambiguous automata, unambiguous Büchi automata, can be used to model check Markov chains. These algorithms are both mathematically elegant and practically efficient for the verification of probabilistic systems. Based on new connections to communication complexity, there has been recent progress around state minimisation and the complexity of language operations on unambiguous automata.