Dynamic Logic of Propositional Assignments

Abstract

Dynamic Logic of Propositional Assignments (DL-PA) is a variant of PDL whose atomic programs are assignments of propositional variables. In DL-PA, quantification over a propositional variable p can be expressed straightforwardly as a nondeterministic choice between assigning p to true and assigning p to false. Conversely, it is less obvious how to find a polynomial translation from DL-PA to QBF. We start by eliminating the Kleene star; then put formulas into a normal form in which all modal operators correspond to Boolean quantifiers; and finally move the quantifiers into prenex form in a polynomial way.

About the Speaker

Andreas Herzig is a CNRS Research Director (Directeur de Recherches CNRS) in the Logic, Interaction, Language, and Computation Group (LILaC) of IRIT at Université Paul Sabatier, France. He served as Head of IRIT’s AI Department from 2009 to 2020 and as Head of the LILaC team from 2000 to 2005. He has been a member of the Scientific Board of CNRS GDR RADIA (formerly GDR IA) since 2016 and of the Executive Board of the CIMI Excellence Laboratory since 2024. He also served on the Scientific Board of the CNRS Institute for Information Sciences and Technologies (INS2I) from 2014 to 2018. He is a Fellow of the European Association for Artificial Intelligence (EurAI), Editor-in-Chief of the Journal of Applied Non-Classical Logics, Associate Editor of Artificial Intelligence, and a member of the Editorial Board of the Journal of Philosophical Logic. He has served on numerous international conference program committees.