24 June 2023, DPFO'23: The Decision Problem in First-Order Logic

[LICS Affiliated Workshop] Nearly a century has now passed since D. Hilbert and W. Ackermann asked if there an algorithm which, when given a formula of first-order logic, determines whether that formula is satisfiable. The negative answer provided by A. Church and A. Turing only a decade later transformed this question into a classification programme: for which fragments of first-order logic, we ask, is the problem of determining the satisfiability of a given formula decidable? Can we chart, in the words of W.V.O. Quine, the limits of decision in first-order logic? Indeed, logicians now typically set themselves a more ambitious goal: given a fragment of first order logic, if its satisfiability (and/or its finite satisfiability problem) is decidable, what is its computational complexity?

From early work on quantifier-prefix fragments, the study of the satisfiability problem (and finite satisfiability problem) for fragments of first-order logic, and indeed of its non-first-order extensions,has now become a central topic in Computational Logic. The aim of the workshop, affiliated with LICS 2023, is to highlight recent developments in this area, with particular emphasis on those fragments which have been the focus of recent interest. These include, for example: Modal and description logics; Logics for ontology-based data access; The negation-guarded fragment; The fluted fragment; Separation logics; Logics of dependence and independence; Combinations of existing fragments.